λ計算機

式または定義を記入して下さい。

例:

• (if true X Y) [この式を評価]
• (car (pair X Y)) [この式を評価]
• (car (cdr (pair X (pair Y Z)))) [この式を評価]
• (succ zero) [この式を評価]
• (succ one) [この式を評価]
• (+ one two) [この式を評価]

既にある定義

(def true (λ t λ f t))
(def false (λ t λ f f))
(def if (λ t λ a λ b t a b))
(def and (λ a λ b a b false))
(def or (λ a λ b a true b))
(def not (λ a a false true))
(def pair (λ ca λ cd λ b b ca cd))
(def car (λ p p true))
(def cdr (λ p p false))
(def zero (λ s λ z z))
(def one (λ s λ z s z))
(def two (λ s λ z s (s z)))
(def succ (λ n λ s λ z s (n s z)))
(def + (λ m λ n λ s λ z m s (n s z)))

ヘルプ

• λ式 'λx.x y' は (λ x x y) 等と表現されます。
• 定義を追加するには、(def シンボル λ式) を入力します。
• free variableは一種の定数として扱われます。free variableがグローバルな定義を持つ場合はそこにリンクが現れ、クリックすると定義に置換されます。
• 適用可能なλ式には、「λ」のところにリンクが現れます。クリックすると、λ式の適用を行います。