ラムダ算

math

定義

  1. 変数はλ式．
  2. （適用）λ式 M，N に対し，MN はλ式．
  3. （抽象）変数 x とλ式 M に対し，λx . M はλ式．
  • 1，2，3からλ式 M が構成されるとき，途中に現れるλ式を M の部分式という．
  • 定義
    1. 変数 x は x の自由変数．
    2. λ式 M，N に対し，変数 x が M の自由変数ならば，x は MN および NM の自由変数．
    3. λ式 M と変数 y に対し，変数 x≠y が M の自由変数ならば，x は λy . M の自由変数．
  • λ式 M の中の自由変数 x をすべてλ式 N に置き換えて得られるλ式を M[x:=N] と書く．

定義 λ式 L の部分式 (λx . M)N を M[x:=N] に置き換えて得られるλ式が L' であるとき，L → L' と書き，これを β簡約 という．

    • λ式はλ式を出力するプログラム，β簡約は実行と思える．