t6s (@t6s)


参加する勉強会



過去の勉強会

11/9 (木)

概要 Martin-Loefの型理論とか勉強しましょう。 (第2回はuniverseの話に費やしたので)第3回は Cohen et al., Cubical Type Theory: a constructive interpretation of the univalence axiom https://arxiv.org/abs/1611.02108 を参考にcubical type theoryをやります。以下の実装も触る予定です。 https://github.com/mortberg/cubicaltt 計画 第一回 intensional / extensional type theory 第二回 universe 第3回 cubical type theory 第?回 observational type theory 第?回 2-dimensional type theory

10/25 (水)

概要 Martin-Loefの型理論とか勉強しましょう。 第2回は Cohen et al., Cubical Type Theory: a constructive interpretation of the univalence axiom https://arxiv.org/abs/1611.02108 を参考にcubical type theoryをやります。以下の実装も触る予定です。 https://github.com/mortberg/cubicaltt 計画 第一回 intensional / extensional type theory 第二回 cubical type theory 第三回 observational type theory

10/5 (木)

概要 Martin-Loefの型理論とか勉強しましょう。 第一回は Hofmann, "Extensional concepts in intensional type theory" http://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/ を参考にしつつ、intensional / extensional type theoryのコア部分をやります。 動く実装があればそれも試すかも 計画 第一回 intensional / extensional type theory 第二回 observational type theory 第三回 cubical type theory

9/17 (日)

台風18号について 台風18号の接近に伴い、17日15時以降名古屋が暴風域に入る可能性があります。 したがって開催時間をはやめ、11:00から14:00くらいに変更します。 作って食べる料理は夕食ではなく昼食となります。 Talkの時間割も変更になると思いますが、現地で決定します。 概要 お茶と料理を楽しみながら関数プログラミングの話とかしましょう。 TOC(台風による予定変更前の内容) 14:00-15:00 Talk 1 依存型の話 (@t6s) 15:00-16:00 お茶 & Talk 2 数学者のいう美しさってなんじゃらほい (@tannakaken) 16:00-17:00 Talk 3 OCaml で線形型を使ったプログラミングの話 (@keigoi) 17:30-20:30 料理と夕食 & Talk 4 分割数の話 (@wasajifu1) お茶 台湾茶 (@GregWeng) 抹茶 (@t6s) 料理 沙茶料理 (@GregWeng) その他 淹れたいお茶などの持ち込み歓迎します

7/27 (木)

量子論理やりましょう。続き物ではなく単発イベントの予定です。 概要 量子論理に関する物理的文脈はさておき,数学的側面に焦点を当てたお話をします. 量子論理では,Hilbert空間の閉部分空間が命題を表現すると考えます. 2次元以上のHilbert空間の閉部分空間全体に包含関係で順序を入れると,分配律を満たさない束になります. これを量子論理と呼ぶことにします. 量子論理における命題に真理値を割り当てる関数は,二値の束準同型写像として与えられます. また,二値の束準同型写像はprime filterと呼ばれるものと対応します. 今回のお話では,束や準同型写像,filterなどの定義を確認してから,分配律と二値の束準同型写像,prime filter間の関係について概観します. そして,量子論理上には二値の束準同型写像が存在しないことを,prime filterを経由して証明します. 参考文献 ・Quantum Logic in Algebraic Approach http://www.springer.com/in/book/9780792349037

7/13 (木)

概要 HFと有限の世界を勉強しましょう。 第11回は[1]のIV.3あたり、encodingをやります。 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.5.8 - IV.5.20 第一不完全性 IV.3 pp.313-317 構文のencoding IV.5.32 第二不完全性 III章 III pp.273- 有限主義 II章 II.18.12 PAとの関係 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346 [3] http://www.kyoritsu-pub.co.jp/bookdetail/9784320110960

6/27 (火)

概要 HFと有限の世界を勉強しましょう。 第10回は[1]のIV.5.20と、IV.5.8の証明を読みます. 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.5.8 - IV.5.20 第一不完全性 IV.3 pp.313-317 構文のencoding IV.5.32 第二不完全性 III章 III pp.273- 有限主義 II章 II.18.12 PAとの関係 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346 [3] http://www.kyoritsu-pub.co.jp/bookdetail/9784320110960

6/9 (金)

概要 HFと有限の世界を勉強しましょう。 第9回は[1]のIV.5.20のあたりを読みます. 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.5.8 - IV.5.20 第一不完全性 IV.3 pp.313-317 構文のencoding IV.5.32 第二不完全性 III章 III pp.273- 有限主義 II章 II.18.12 PAとの関係 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346

5/23 (火)

概要 HFと有限の世界を勉強しましょう。 第8回は[1]のIV.5.18のあたりを読みます. 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.5.8 - IV.5.20 第一不完全性 IV.3 pp.313-317 構文のencoding IV.5.32 第二不完全性 III章 III pp.273- 有限主義 II章 II.18.12 PAとの関係 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346

5/11 (木)

概要 HFと有限の世界を勉強しましょう。 第7回は[1]のIV.5.9、第一不完全性定理のあたりを読みます. 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST III章 III pp.273- 有限主義 IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.3 pp.313- 構文のencoding ... (この辺未定; [2]も参照しつつやる) IV.5.32 第二不完全性 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346

4/20 (木)

概要 HFと有限の世界を勉強しましょう。 第6回は[1]の IV.3.11のあたりを読みます. 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST III章 III pp.273- 有限主義 IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.3 pp.313- 構文のencoding ... (この辺未定; [2]も参照しつつやる) IV.5.32 第二不完全性 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346

4/13 (木)

296b2164278476aab6af688fe488197e 『FP in Scala』読書会@名古屋
目的 『Scala関数型デザイン&プログラミング』(FP in Scala)を読み、練習問題を解くことで、関数型プログラミングの考えやScala言語を楽しく学ぶ。 今回の範囲 第10章 モノイドの10.5節 からです。事前にしっかりExerciseを解いておくのをオススメします。 進め方 参加者でさらっと読み合わせる Exerciseも解く みんなで疑問点を質問、解消していく Scala有識者から解説もらってハッピーになる 今回から参加でも大丈夫 対象者 最近話題のScalaを独学してみたけど、挫折しちゃった方 なごやかScalaに参加したかったけど、もう終わってて悔しかった方 名古屋に住んでおきながら関数型プログラミングを知らない事に負い目を感じている方 関数型プログラミングの勉強会に行ったけど、みんなが何言ってるか分からず挫折した方 関数型プログラミングとかよく分からないけど、みんなとプログラミングの勉強を楽しみたい方 持ち物 『Scala関数型デザイン&プログラミング』 ノートPC(任意)。Exerciseを解くのに使います Scalaをみんなと一緒に楽しく学ぼうという気持ち 場所 来栖川電算 会議室 名古屋市中区新栄1丁目29-23 アーバンドエル新栄2階 地下鉄鶴舞線 鶴舞駅から徒歩11分 JR中央本 鶴舞駅から徒歩11分

4/2 (日)

3e245a14de34587bf7cab47fc8af1dd0 CoderDojo名古屋
メンターさん対象です!
CoderDojo 名古屋のメンターさんの参加表明です セッションの内容は別途、例会案内を御覧ください はじめての方は管理者へ別途連絡下さい

3/29 (水)

概要 HFと有限の世界を勉強しましょう。 第5回は[1]の IV.3.9, IV.3.11のあたりを読みます. 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST III章 III pp.273- 有限主義 IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.3 pp.313- 構文のencoding ... (この辺未定; [2]も参照しつつやる) IV.5.32 第二不完全性 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346

3/25 (土)

1b387458e5304c0b38543632c29d9473 CoderDojo天白
メンターさん、、対象です!
CoderDojo天白のメンターさん宛のイベント告知です 新しく、メンターを希望される方もこちらに参加下さい。また、イベント管理者へ連絡下さい。 午前 通常の例会 午後 スクラッチ入門 詳細は各イベント告知ページをご覧ください。 メンター希望の方は、いろんな知識・経験を持ったメンターを募集しています。当然、IT関連の人、プログラマーは歓迎ですが、子どもたちに接して、会を盛り上げてくれる人もまた、大歓迎です。

3/18 (土)

1b387458e5304c0b38543632c29d9473 CoderDojo天白
メンターさん、、対象です!
CoderDojo天白のメンターさん宛のイベント告知です 新しく、メンターを希望される方もこちらに参加下さい。また、イベント管理者へ連絡下さい。 午前 通常の例会 午後 スクラッチ入門 詳細は各イベント告知ページをご覧ください。 メンター希望の方は、いろんな知識・経験を持ったメンターを募集しています。当然、IT関連の人、プログラマーは歓迎ですが、子どもたちに接して、会を盛り上げてくれる人もまた、大歓迎です。

3/10 (金)

概要 HFと有限の世界を勉強しましょう。 第4回は[1]の IV.1からIV.3のあたりを読みます. (II.18 弱い集合論 は後回し) 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST III章 III pp.273- 有限主義 IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.3 pp.313- 構文のencoding ... (この辺未定; [2]も参照しつつやる) IV.5.32 第二不完全性 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346

2/11 (土)

参加希望の方は、 ATNDで参加表明をして、更に 参加申し込みフォーム(ここをクリック) で登録してください。 申し込み期限:2017年1月31日 参加費なし 二日間にわたって、物理と幾何に関連して講演と討論を行います。 世話人 後藤振一郎 谷村省吾 深川宏樹 お願い:会場には公共交通機関を利用しておこしください。近隣での自家用車の路上駐車・無断駐車はくれぐれもお控えください。 研究会プログラム.pdf(ここをクリック) 1日目:2017年2月11日(土) 座長 後藤振一郎 10:00-11:20 秋元琢磨 11:30-12:50 横倉祐貴 座長 中田陽介 14:00-15:20 野田知宣 15:30-16:50 後藤振一郎 17:00-18:20 三嶋宏章 19:00-21:00 懇親会 グランピアット 4000円前後の予定 ぐるナビ(ここをクリック) 2日目:2017年2月12日(日) 座長 古賀実 9:30-11:00 谷村省吾 11:10-12:40 檜山正幸 座長 深川宏樹  14:00-15:30 春名太一 15:40-17:10 村主崇行 講演内容 一日目 ====== 秋元琢磨 | 慶應義塾大学 「大数の法則の破れと異常拡散」 微小粒子を水に浮かべると、あたかも生命を持った物体のような不規則な運動を行う。この運動は、ブラウン運動としてよく知られた物理現象であり、平均2乗変位(MSD)により特徴づけられる。通常の場合、MSDは時間に対して線形に増大し、その傾きがその運動の拡散性を表す。この拡散性は、微粒子の静的な構造(形状や表面の性質等)と媒質により決定される。本講演では、媒質が均一ではなく、局所的な拡散性がランダムに分布している場合、長時間の観測により得られる拡散性はどのようになるのか?という基礎的な疑問に答えたい。素朴に考えると、系が十分に大きければ、観測結果は、局所的な拡散性を全体で平した平均的な振る舞いになると予想される。数学的には、大数の法則がこの結果を示唆している。ここでは、不均質な系のモデルとして、時間的に変化しないランダムなポテンシャルエネルギー空間上のランダムウォークを考える。我々は、ある温度(ガラス温度)以下では、この系の拡散性は、たとえ系のサイズを大きくしても、同じ値には収束せず、系の不均質性に強く依存することを明らかにする。換言すれば、大数の法則が破れ、拡散性は系に依存して本質的にランダムになることを示す。 横倉祐貴 | 理化学研究所iTHES 「ネーター不変量としての熱力学エントロピー」 (Thermodynamic entropy as a Noether invariant) We first study a classical many-particle system with an external control represented by a time-dependent extensive parameter in a Lagrangian. We show that thermodynamic entropy of the system is uniquely characterized as the Noether invariant associated with a symmetry for an infinitesimal non-uniform time translation, where trajectories in the phase space are restricted to those consistent with quasi-static processes in thermodynamics. Then, a universal constant of the action dimension appears, although there is no such a constant in the classical mechanics. Furthermore, we discuss thermally isolated quantum many-body systems with time dependent external operation. From the unitary time evolution of quantum pure states, we derive an effective action for trajectories in the thermodynamic state space. In the action, the entropy appears with its conjugate variable, and a symmetry emerges leading to the entropy as a Noether invariant. This can be understood as the origin of the symmetry found in the classical mechanics. 野田知宣 | 明治薬科大学 薬学部 「正準変換による時間発展について」 シンプレクティック幾何学を通じて情報幾何学、量子力学、Bayes 統計などの繋がりについて概説する。 後藤振一郎 | 京都大学情報学研究科 「電気回路系の接触幾何学的および情報幾何学的記述」 電圧源なしの電気回路系を表現する力学系は接触多様体上で定式化され得ることを示す。また、この幾何学的定式化により、情報幾何学と平衡熱力学と電気回路系が統一的に扱える可能性を指摘する。 三嶋宏章 | 名古屋大学情報科学研究科 「量子系の有限時間断熱制御と力学不変量」 量子系の外部パラメタを「無限の時間をかけて、限りなくゆっくりと」動かせば、系の時間発展は断熱変化(エネルギー固有状態間の遷移を伴わない時間発展)になることが、量子断熱定理として知られている。しかし、実用的な問題を考えるならば、「限りなくゆっくりと」という条件は取り払いたい。Shortcuts to Adiabaticity (STA) と呼ばれる手法を用いると、理論的には、任意の有限時間内に断熱変化を達成できる。このような時間短縮された量子系のダイナミクスを、力学不変量と断熱性から特徴付ける。 二日目 ====== 谷村省吾 |名古屋大学情報科学研究科 「物理学者のための圏論入門」 圏論にまったくなじみのない方向けの入門的な講演です。射・関手・自然変換・直積・直和・極限・余極限などの基本概念を解説します。例として、ホモトピー関手を導入したいと思います。 檜山正幸 |檜山正幸事務所 「事例とストリング図によるn-圏への入門」 詳細は、 http://d.hatena.ne.jp/m-hiyama/20161031/1477878381 春名太一 | 神戸大学理学研究科惑星学専攻 「複雑ネットワークと圏論」 生物などにみられる現実世界の複雑ネットワークでは、 頂点はただの点ではなく「はたらき」を持ち、頂点の「はたらき」が貼り合わさ れてネットワーク全体が構成されている、と考えることが自然な場合があるよう に思えます。本講演では、このような観点を圏論を用いて理論化することでみえ てきた、複雑ネットワークの新たな側面について紹介します。 村主崇行 | 理化学研究所 計算科学研究機構 「偏微分方程式から高性能プログラムへの自動変換」 今日のシミュレーション科学を支えるスーパーコンピュータは数十万から数億ものスレッドを並列に実行する能力を持ち、その全てに適切に仕事を割り振ってやらない限り性能を完全に引き出すことはできません。そのため、今日のシミュレーションプログラムはときに数十万行にもおよび、それを書く仕事は大変なものです。ですが、原理的にはそのようなプログラムは、シミュレートしたい方程式と、その離散化法を指定してやれば機械的に生成できるはずです。シミュレートしたい物理系が元来そなえている並列性と局所性を、計算機の並列性と局所性にマップしてやればよいのです。このトークではそれを実現するための手法についてお話します。 昼ごはん情報 ■お昼ごはんについて 土曜は会場近く(徒歩3分程度)の学食が,11:00~14:00の間営業しています(日曜は閉まっています): 学食url 近くに飲食店が幾つかあります. ・牡丹亭 (中華料理) 牡丹亭 url ・香蘭楼(中華料理) 香蘭楼url ・海鮮館(台湾料理) 海鮮館url 以上の3店舗は,お昼の時間は混んでいることが多いです. ・ハロキ(ハンバーグ) ハロキurl ・グランピアット(イタリアン) グランピアットurl 「デリデリ 四ツ谷通店」 デリデリurl は、テイクアウトも可能 (ただ、会場となる建物から、若干遠い) モスバーガー本山四谷通店 モスバーガーurl (ちょっと遠い) ファミリーマート (会場に近い) 交通案内 会場:名古屋大学情報科学研究科棟 1階 第1講義室 ↓この地図のA4(3) アクセスマップ アクセスPDF Google map 交通案内: 交通案内 ウェブサイト JR名古屋駅から名古屋大学東山キャンパスに公共交通機関で来る場合 1) JR名古屋駅から 地下鉄東山線で 本山駅まで (約15分) 2) 本山駅で地下鉄名城線(右回り)に乗り換えて(乗り換え待ち時間最大10分)名古屋大学駅まで (約1分) 3) 名古屋大学駅1番出口から出て情報科学研究科棟(情科棟)まで徒歩(約10分)  情科棟は8階建ての建物(この周辺では一番高い建物)  情科棟玄関から入ってすぐ右側が第1講義室

1b387458e5304c0b38543632c29d9473 CoderDojo天白
メンターさん、、対象です!
CoderDojo天白のメンターさん宛のイベント告知です 新しく、メンターを希望される方もこちらに参加下さい。また、イベント管理者へ連絡下さい。 午前 通常の例会 午後 スクラッチ入門 詳細は各イベント告知ページをご覧ください。 メンター希望の方は、いろんな知識・経験を持ったメンターを募集しています。当然、IT関連の人、プログラマーは歓迎ですが、子どもたちに接して、会を盛り上げてくれる人もまた、大歓迎です。

2/9 (木)

概要 HFと有限の世界を勉強しましょう。 第3回は[1]の pp.119- HF<ω ⊂ HF などを読みます。 予習不要 計画 I章 p.107 HFの定義 p.119 データ構造の例 II章 II.17 Δ0 II.17.21 Σ1, Π1 II.18 CST III章 III pp.273- 有限主義 IV章 IV pp.289- (ω| HF)上(Δ0|Δ1) IV.3.1 HFでの決定可能性, 計算可能性 IV.3 pp.313- 構文のencoding ... (この辺未定; [2]も参照しつつやる) IV.5.32 第二不完全性 教科書 [1] https://www.nippyo.co.jp/shop/book/7176.html 参考書 [2] https://www.amazon.co.jp/Incompleteness-Land-Sets-Studies-Logic/dp/1904987346