dotimesマクロ #cielo_ee_only [XP64]

posted at 23:42:01

M⇒NかつNがβ基をもたないなら、Mは正規形Nをもつ #cielo_ee_only [X60s]

posted at 00:13:05

変換可能なβ基が複数ある場合、変換の方法によっては有限回で終わらない場合もある #cielo_ee_only [X60s]

posted at 00:14:38

正規化定理：λ式Mが正規形Nを持てば、できるだけ外側および左側からβ変換を行えば、MからNに変換できる #cielo_ee_only [X60s]

posted at 00:26:01

自然数をλ式で定義する。Church符号化 #cielo_ee_only [X60s]

posted at 00:29:10

さっきのChurch符号化であらわされた自然数、たとえばsに１＋という関数を適用するとそのまんま自然数になる #cielo_ee_only

posted at 00:44:13

分かってきたところで別のλ計算の例を探してみよう #cielo_ee_only [X60s]

posted at 00:45:51

λx.MのMは関数の実体で、たとえばx^2とかx+1みたいなもの #cielo_ee_only [X60s]

posted at 21:15:43

関数抽象とはMをxの関数とみなすこと #cielo_ee_only [X60s]

posted at 21:17:50

関数適用とは引数によって関数を呼び出すこと。直感的にいうと代入みたいなもの #cielo_ee_only [X60s]

posted at 21:26:20

１ページ目で挫折 #cielo_ee_only [X60s]

posted at 21:39:47

MNが関数適応(例：(λx.x^2)3 はxに3を代入すること #cielo_ee_only [X60s]

posted at 21:42:52

定義域がない関数におけるλ計算を型無しλ計算という #cielo_ee_only [X60s]

posted at 21:45:04

λ式の中の(λx.M)Nのような部分をβ基という #cielo_ee_only [X60s]

posted at 21:56:59

Mの中のすべての変数xをNに置き換える操作をβ変換という #cielo_ee_only [X60s]

posted at 21:58:22

β変換って単に代入して計算することと同じ気がするんだけど、そういう理解でいいのかな #cielo_ee_only [X60s]

posted at 22:00:17

また束縛とかいう単語が定義なしで出てきた・・・ #cielo_ee_only [X60s]

posted at 22:02:31

xが関数Ｋの局所変数であることを、変数xがKに束縛されているという #cielo_ee_only [X60s]

posted at 22:41:19

そこでーβ変換では、関連していない変数は名前が重複していないという条件をつける #cielo_ee_only [X60s]

posted at 22:43:16

λy.(λx.xy)xのyにxを適用するとおかしなことになってしまうというのが例 #cielo_ee_only [X60s]

posted at 22:47:46

一般に、β変換を行う順番で最終的な結果は変わる #cielo_ee_only [X60s]

posted at 22:49:29

はてなキーワードみると、β簡約はプログラミング言語でいうとインライン展開みたいなもんだとか書いてあるが #cielo_ee_only [X60s]

posted at 22:58:42

どこがβ基なのかわからないんですが #cielo_ee_only [X60s]

posted at 23:08:23

形式的にはどうすればいいかわかってきたがそんなことでいいのか・・・ #cielo_ee_only [X60s]

posted at 23:27:23

(λx.M)NのM内のxを全てMで置き換えたら、xはなくなってしまうので先頭のλxはきえてもいいのか #cielo_ee_only [X60s]

posted at 23:32:42

((λz.xz)(λz.z))のどこがβ基なんだ？ #cielo_ee_only [X60s]

posted at 23:36:25

λ式によって定義された自然数をチャーチ数という #cielo_ee_only [X60s]

posted at 00:01:08

演算も定義できるっというか何でも定義できる #cielo_ee_only [X60s]

posted at 00:01:30

簡約のルールが分かれば分かりそうだ #cielo_ee_only [X60s]

posted at 00:02:00

えっと、複数の述語を組み合わせるところまで行ったんだった #cielo_ee_only [X60s]

posted at 21:34:35

マクロ？ #cielo_ee_only [X60s]

posted at 21:35:02

S式はラムダ計算を(ry なるほど #cielo_ee_only [X60s]

posted at 21:39:23

あれ、評価結果ってnil以外はtになるんだっけ #cielo_ee_only [X60s]

posted at 21:46:06

ちがった、<とかの戻り値が元々tかnilだから当たり前か #cielo_ee_only [X60s]

posted at 21:46:36

次は条件分岐 #cielo_ee_only [X60s]

posted at 21:46:51

(if <条件部> <then節> <else節>) #cielo_ee_only [X60s]

posted at 21:47:50

なんかあれだ、初めての言語やるときは細かいところで悩むよりどんどん進んだほうがいい気がする。 #cielo_ee_only [X60s]

posted at 21:51:43

というわけで次に行く #cielo_ee_only [X60s]

posted at 21:51:52

なんかこうしてみると最初は面食らうけどあんまり手続き型言語と変わらん気もするが #cielo_ee_only [X60s]

posted at 21:54:08

whenとunlessも普通か #cielo_ee_only [X60s]

posted at 21:55:03

条件分岐はcondを使うと #cielo_ee_only [X60s]

posted at 21:57:55

次は再起定義？ #cielo_ee_only [X60s]

posted at 21:59:26

あれ、*ってなんの記号だっけ・・・ #cielo_ee_only

posted at 22:03:07

あ、普通に掛け算だった #cielo_ee_only

posted at 22:05:57

ちょっとちゃんと背景の勉強をしたい #cielo_ee_only

posted at 22:14:59

wikipediaのラムダ計算の所見てもちっともわからんのですが #cielo_ee_only

posted at 22:18:17

この辺を見ながら http://bit.ly/bayjN5 #cielo_ee_only [X60s]

posted at 22:55:44

ラムダ計算の式を項という #cielo_ee_only

posted at 22:56:10

変数は項になる。関数内では束縛変数か自由変数になる #cielo_ee_only

posted at 22:57:08

関数を作る構文を抽象という #cielo_ee_only

posted at 22:57:43

たとえばλみなぜ.み ぜ(な ぜ) とλ(ぜなみ).ぜ み（な み）はα同値である #cielo_ee_only [X60s]

posted at 23:49:15

ラムダ計算の式を実行することを簡約という #cielo_ee_only [X60s]

posted at 23:50:19

(λx.λy.x) ab→(λy.a)b→a #cielo_ee_only [X60s]

posted at 23:54:00

違った、消えたのはbのほうか #cielo_ee_only [X60s]

posted at 23:55:51

これ以上簡約できない項のことを正規系という #cielo_ee_only [X60s]

posted at 23:57:15

正規系にならずに無限ループになることもある #cielo_ee_only [X60s]

posted at 23:58:08