(* ungetypter Lambda-Kalkuel - Reduktion *) (* Vigano/Leven/Friedrich/Ayari WS00/01 *) RED = Pure + types term consts Abs :: "[term => term] => term" (binder "lam " 10) "^" :: "[term, term] => term" (infixl 20) K :: "term" I :: "term" S :: "term" B :: "term" YC :: "term" YT :: "term" Trueprop :: "[term, term] => prop" ("(_ --> _)") rules beta "(lam x. f(x))^a --> f(a)" refl "M --> M" trans "[| M --> N; N --> L |] ==> M --> L" appr "M --> N ==> M^Z --> N^Z" appl "M --> N ==> Z^M --> Z^N" epsi "[| !!x. M(x) --> N(x) |] ==> (lam x. M(x)) --> (lam x. N(x))" K_def "K == lam x. (lam y. x)" I_def "I == lam x. x" S_def "S == lam x. (lam y. (lam z. x^z^(y^z)))" B_def "B == S^(K^S)^K" YC_def "YC == lam f. ((lam x. f^(x^x))^(lam x. f^(x^x)))" YT_def "YT == (lam z. lam x. x^(z^z^x))^(lam z. lam x. x^(z^z^x))" syntax (symbols) "lam " :: "[idts, term] => term" ("(3\\_./ _)" [0, 10] 10) syntax (xsymbols) "op -->" :: "[term, term] => term" (infixr "\\" 25) end