[윤용호]

(* open Lam *)

let le1=App (Lam ("x", Var "y"), Lam ("z", Var "z"))
let le2=Lam("y", App (Lam ("x", Var "y"), Lam ("z", Var "z")))
let le3=App((Lam ("x", App (Lam ("y", App (Var "y", Var "x")), Var "z"))), App (Var "z", Var "w"))
let le4=Lam ("z", Lam ("w", App((Lam ("x", App (Lam ("y", App (Var "y", Var "x")), Var "z"))), App (Var "z", Var "w"))))
let le5=App(Lam ("x", App(Var "x", Var "x")), Lam ("y", App(Var "y", Var "y")))
let le6=App(Lam ("w", App(Lam ("z", Var "w"), App(Lam ("x", App(Var "x", Var "x")), Lam ("y", App(Var "y", Var "y"))))), Lam ("a", Var "a"))
let le7=App(Lam ("x", Lam ("a", Lam ("b", App(App(Var "a", Var "x"), App(Var "b", Var "x"))))), Lam("y", Var "y"))
let le8=App(Lam ("x", Lam ("a", Lam ("b", Lam ("c", App(App(App(Var "a", Var "x"), App(Var "b", Var "x")), App(Var "c", Var "x")))))), Lam ("y", Var "y"))
let le9=Lam("c", App(App(Var "c", le7), Lam("y'", Var "y'")))
let l_zero = Lam("f_zero", Lam ("x_zero", Var "x_zero"))
let l_one = Lam("f_one", Lam ("x_one", App(Var "f_one", Var "x_one")))
let l_succ = Lam("n", Lam ("f_succ", Lam ("x_succ", App(Var "f_succ", App(App(Var "n", Var "f_succ"), Var "x_succ")))))
let l_add = Lam ("n1", Lam ("n2", Lam ("f_add", Lam ("x_add", App(App(Var "n1", Var "f_add"), App(App(Var "n2", Var "f_add"), Var "x_add"))))))
let l_mult = Lam ("n1", Lam ("n2", Lam ("f_mult", App(Var "n1", App(Var "n2", Var "f_mult")))))
let l_two = App(l_succ, l_one)
let l_three = App(App(l_add, App(l_succ, (Lam("f_two", Lam ("x_two", App(Var "f_two", Var "x_two")))))), (Lam("f_three", Lam ("x_three", App(Var "f_three", Var "x_three")))))
let l_six = App(App(l_mult, (Lam ("f_two", Lam("x_two", App(Var "f_two", App(Var "f_two", Var "x_two")))))), (Lam ("f_three", Lam("x_three", App(Var "f_three", App(Var "f_three", App(Var "f_three", Var "x_three")))))))
let test () = ignore (
print_endline ">>le2 result : \\(y).y";
pp le2;
pp(reduce le2);
print_newline();print_endline ">>le4 result : \\(z).\\(w).(z (z w))";
pp le4;
pp(reduce le4);
print_newline();print_endline ">>le6(non infinite loop) result : \\(a).a";
pp le6;
pp(reduce le6);
print_newline();print_endline ">>le7 result : \\(a).\\(b).((a \\(y).y) (b \\(y').y'))";
pp le7;
pp(reduce le7);
print_newline();print_endline ">>le8 result : \\(a).\\(b).\\(c).(((a \\(y).y) (b \\(y').y')) (c \\(y'').y''))";
pp le8;
pp(reduce le8);
print_newline();print_endline ">>le9 result : \\(c).((c \\(a).\\(b).((a \\(y).y) (b \\(y'').y''))) \\(y').y')";
pp le9;
pp(reduce le9);
print_newline();print_endline ">>l_two result : \\(f_succ).\\(x_succ).(f_succ (f_succ x_succ))";
pp l_two;
pp(reduce l_two);
print_newline();print_endline ">>l_three result : \\(f_add).\\(x_add).(f_add (f_add (f_add x_add)))";
pp l_three;
pp(reduce l_three);
print_newline();print_endline ">>l_six result : \\(f_mult).\\(x_two).(f_mult (f_mult (f_mult (f_mult (f_mult (f_mult x_two))))))";
pp l_six;
pp(reduce l_six);
print_newline();print_endline ">>le5(infinite loop)... use \"Ctrl+C\" to halt";
pp le5;
pp(reduce le5)
)

Lam을 open 하고 interpreter에 넣거나
아예 이 코드를 module 안에 넣으셔도 됩니다.
(module 안에 넣을 경우는 test()를 호출할수 없으므로 sig에 matching 시키시면 안되구요)

실행은 test () 을 입력합니다. (module에 넣은 경우 Lam.test()가 되겠지요..)

le9 같은 경우 본인 구현에 맞게 적당히 바꾸어 사용하세요.
저같은 경우 새 이름 만들때 ' 을 붙이게 되어있어서
x에 \y.y를 대입할 때 외부에 있는 \y'.y'과 일부러 충돌이 일어나게 만들어서 \y''.y'' 이 생성되도록 했습니다.
_________________
TA

[윤용호]

(* open Debru *)
let de2=L(A(L(N 1), L(N 0)))
let de4=L(L(A(L(A(L(A(N 0, N 1)), N 2)), A(N 1, N 0))))
let de5=A(L(A(N 0, N 0)), L(A(N 0, N 0)))
let de6=A(L(A(L(N 1), A(L(A(N 0, N 0)), L(A(N 0, N 0))))), L(N 0))
let de7=A(L(L(L(A(A(N 1, N 2), A(N 0, N 2))))), L(N 0))
let de8=A(L(L(L(L(A(A(A(N 2, N 3), A(N 1, N 3)), A(N 0, N 3)))))), L(N 0))
let de9=L(A(A(N 0, de7), L(N 0)))
let d_zero = L(L(N 0))
let d_one = L(L(A(N 1, N 0)))
let d_succ = L(L(L(A(N 1, A(A(N 2, N 1), N 0)))))
let d_add = L(L(L(L(A(A(N 3, N 1), A(A(N 2, N 1), N 0))))))
let d_mult = L(L(L(A(N 2, A(N 1, N 0)))))
let d_two = A(d_succ, d_one)
let d_three = A(A(d_add, d_one), d_two)
let d_four = A(A(d_mult, d_two), d_two)
let d_five = A(A(d_add, d_three), d_two)
let d_six = A(A(d_mult, d_two), d_three)

let test() = ignore(
print_endline ">>de2 result : L.0";
pp de2;
pp(reduce de2);
print_newline();print_endline ">>de4 result : L.L.(1 (1 0))";
pp de4;
pp(reduce de4);
print_newline();print_endline ">>de6 result : L.0";
pp de6;
pp(reduce de6);
print_newline();print_endline ">>de7 result : L.L.((1 L.0) (0 L.0))";
pp de7;
pp(reduce de7);
print_newline();print_endline ">>de8 result : L.L.L.(((2 L.0) (1 L.0)) (0 L.0))";
pp de8;
pp(reduce de8);
print_newline();print_endline ">>de9 result : L.((0 L.L.((1 L.0) (0 L.0))) L.0)";
pp de9;
pp(reduce de9);
print_newline();print_endline ">>d_two result : L.L.(1 (1 0))";
pp d_two;
pp(reduce d_two);
print_newline();print_endline ">>d_three result : L.L.(1 (1 (1 0)))";
pp d_three;
pp(reduce d_three);
print_newline();print_endline ">>d_four result : L.L.(1 (1 (1 (1 0))))";
pp d_four;
pp(reduce d_four);
print_newline();print_endline ">>d_five result : L.L.(1 (1 (1 (1 (1 0)))))";
pp d_five;
pp(reduce d_five);
print_newline();print_endline ">>d_six result : L.L.(1 (1 (1 (1 (1 (1 0))))))";
pp d_six;
pp(reduce d_six);
print_newline();print_endline ">>de5(infinite loop)... use \"Ctrl+C\" to halt";
pp de5;
pp(reduce de5)
)

사용법은 1번 testset과 동일합니다.
대부분의 testset이 1번 testset을 그대로 Debru 로 옮긴 것들입니다.

덧붙여 테스트셋들에 대한 약간의 해설을 하자면
e5같은 경우 대표적인 "무한히 도는 lambda식" 이고
zero, one, succ, add, mult 등의 경우 lambda로 encoding 된 자연수 표현입니다. \f.\x.((f^n) x) 로 인코딩되어 있습니다.(f의 등장횟수가 수를 나타냅니다)

그밖에도 true, false, pair, if-then-else 등이 모두 lambda로 인코딩 가능하지만
우리가 받은 lambda expression의 스펙이 이름이 겹치는걸 허용하지 않아
그것들을 이용한 의미있는 테스트셋을 만들기 어렵더군요.
_________________
TA

[윤용호]

module T = Trans (Lam) (Debru)

let le1=Lam.App (Lam.Lam ("x", Lam.Var "y"), Lam.Lam ("z", Lam.Var "z"))
let le2=Lam.Lam("y", Lam.App (Lam.Lam ("x", Lam.Var "y"), Lam.Lam ("z", Lam.Var "z")))
let le3=Lam.App((Lam.Lam ("x", Lam.App (Lam.Lam ("y", Lam.App (Lam.Var "y", Lam.Var "x")), Lam.Var "z"))), Lam.App (Lam.Var "z", Lam.Var "w"))
let le4=Lam.Lam ("z", Lam.Lam ("w", Lam.App((Lam.Lam ("x", Lam.App (Lam.Lam ("y", Lam.App (Lam.Var "y", Lam.Var "x")), Lam.Var "z"))), Lam.App (Lam.Var "z", Lam.Var "w"))))
let le5=Lam.App(Lam.Lam ("x", Lam.App(Lam.Var "x", Lam.Var "x")), Lam.Lam ("y", Lam.App(Lam.Var "y", Lam.Var "y")))
let le6=Lam.App(Lam.Lam ("w", Lam.App(Lam.Lam ("z", Lam.Var "w"), Lam.App(Lam.Lam ("x", Lam.App(Lam.Var "x", Lam.Var "x")), Lam.Lam ("y", Lam.App(Lam.Var "y", Lam.Var "y"))))), Lam.Lam ("a", Lam.Var "a"))
let le7=Lam.App(Lam.Lam ("x", Lam.Lam ("a", Lam.Lam ("b", Lam.App(Lam.App(Lam.Var "a", Lam.Var "x"), Lam.App(Lam.Var "b", Lam.Var "x"))))), Lam.Lam("y", Lam.Var "y"))
let le8=Lam.App(Lam.Lam ("x", Lam.Lam ("a", Lam.Lam ("b", Lam.Lam ("c", Lam.App(Lam.App(Lam.App(Lam.Var "a", Lam.Var "x"), Lam.App(Lam.Var "b", Lam.Var "x")), Lam.App(Lam.Var "c", Lam.Var "x")))))), Lam.Lam ("y", Lam.Var "y"))
let le9=Lam.Lam("c", Lam.App(Lam.App(Lam.Var "c", le7), Lam.Lam("y'", Lam.Var "y'")))
let l_zero = Lam.Lam("f_zero", Lam.Lam ("x_zero", Lam.Var "x_zero"))
let l_one = Lam.Lam("f_one", Lam.Lam ("x_one", Lam.App(Lam.Var "f_one", Lam.Var "x_one")))
let l_succ = Lam.Lam("n", Lam.Lam ("f_succ", Lam.Lam ("x_succ", Lam.App(Lam.Var "f_succ", Lam.App(Lam.App(Lam.Var "n", Lam.Var "f_succ"), Lam.Var "x_succ")))))
let l_add = Lam.Lam ("n1", Lam.Lam ("n2", Lam.Lam ("f_add", Lam.Lam ("x_add", Lam.App(Lam.App(Lam.Var "n1", Lam.Var "f_add"), Lam.App(Lam.App(Lam.Var "n2", Lam.Var "f_add"), Lam.Var "x_add"))))))
let l_mult = Lam.Lam ("n1", Lam.Lam ("n2", Lam.Lam ("f_mult", Lam.App(Lam.Var "n1", Lam.App(Lam.Var "n2", Lam.Var "f_mult")))))
let l_two = Lam.App(l_succ, l_one)
let l_three = Lam.App(Lam.App(l_add, Lam.App(l_succ, (Lam.Lam("f_two", Lam.Lam ("x_two", Lam.App(Lam.Var "f_two", Lam.Var "x_two")))))), (Lam.Lam("f_three", Lam.Lam ("x_three", Lam.App(Lam.Var "f_three", Lam.Var "x_three")))))
let l_six = Lam.App(Lam.App(l_mult, (Lam.Lam ("f_two", Lam.Lam("x_two", Lam.App(Lam.Var "f_two", Lam.App(Lam.Var "f_two", Lam.Var "x_two")))))), (Lam.Lam ("f_three", Lam.Lam("x_three", Lam.App(Lam.Var "f_three", Lam.App(Lam.Var "f_three", Lam.App(Lam.Var "f_three", Lam.Var "x_three")))))))

let de2=Debru.L(Debru.A(Debru.L(Debru.N 1), Debru.L(Debru.N 0)))
let de4=Debru.L(Debru.L(Debru.A(Debru.L(Debru.A(Debru.L(Debru.A(Debru.N 0, Debru.N 1)), Debru.N 2)), Debru.A(Debru.N 1, Debru.N 0))))
let de5=Debru.A(Debru.L(Debru.A(Debru.N 0, Debru.N 0)), Debru.L(Debru.A(Debru.N 0, Debru.N 0)))
let de6=Debru.A(Debru.L(Debru.A(Debru.L(Debru.N 1), Debru.A(Debru.L(Debru.A(Debru.N 0, Debru.N 0)), Debru.L(Debru.A(Debru.N 0, Debru.N 0))))), Debru.L(Debru.N 0))
let de7=Debru.A(Debru.L(Debru.L(Debru.L(Debru.A(Debru.A(Debru.N 1, Debru.N 2), Debru.A(Debru.N 0, Debru.N 2))))), Debru.L(Debru.N 0))
let de8=Debru.A(Debru.L(Debru.L(Debru.L(Debru.L(Debru.A(Debru.A(Debru.A(Debru.N 2, Debru.N 3), Debru.A(Debru.N 1, Debru.N 3)), Debru.A(Debru.N 0, Debru.N 3)))))), Debru.L(Debru.N 0))
let de9=Debru.L(Debru.A(Debru.A(Debru.N 0, de7), Debru.L(Debru.N 0)))
let d_zero = Debru.L(Debru.L(Debru.N 0))
let d_one = Debru.L(Debru.L(Debru.A(Debru.N 1, Debru.N 0)))
let d_succ = Debru.L(Debru.L(Debru.L(Debru.A(Debru.N 1, Debru.A(Debru.A(Debru.N 2, Debru.N 1), Debru.N 0)))))
let d_add = Debru.L(Debru.L(Debru.L(Debru.L(Debru.A(Debru.A(Debru.N 3, Debru.N 1), Debru.A(Debru.A(Debru.N 2, Debru.N 1), Debru.N 0))))))
let d_mult = Debru.L(Debru.L(Debru.L(Debru.A(Debru.N 2, Debru.A(Debru.N 1, Debru.N 0)))))
let d_two = Debru.A(d_succ, d_one)
let d_three = Debru.A(Debru.A(d_add, d_one), d_two)
let d_four = Debru.A(Debru.A(d_mult, d_two), d_two)
let d_five = Debru.A(Debru.A(d_add, d_three), d_two)
let d_six = Debru.A(Debru.A(d_mult, d_two), d_three)

let _ = ignore (
print_endline "/**************transl2d test***************/";
print_endline ">> de2=trans(le2) & original de2";
Debru.pp (T.transl2d le2);
Debru.pp de2;
print_newline();print_endline ">> de4=trans(le4) & original de4";
Debru.pp (T.transl2d le4);
Debru.pp de4;
print_newline();print_endline ">> de5=trans(le5) & original de5";
Debru.pp (T.transl2d le5);
Debru.pp de5;
print_newline();print_endline ">> de6=trans(le6) & original de6";
Debru.pp (T.transl2d le6);
Debru.pp de6;
print_newline();print_endline ">> de7=trans(le7) & original de7";
Debru.pp (T.transl2d le7);
Debru.pp de7;
print_newline();print_endline ">> de8=trans(le8) & original de8";
Debru.pp (T.transl2d le8);
Debru.pp de8;
print_newline();print_endline ">> de9=trans(le9) & original de9";
Debru.pp (T.transl2d le9);
Debru.pp de9;
print_newline();print_endline "/**************transd2l test***************/";
print_endline ">> transl2d(reduce(transd2l(de2))) & reduce(de2)";
Lam.pp (T.transd2l de2);
Lam.pp le2;
Debru.pp (T.transl2d (Lam.reduce (T.transd2l de2)));
Debru.pp (Debru.reduce de2);
print_newline();print_endline ">> transl2d(reduce(transd2l(de4))) & reduce(de4)";
Lam.pp (T.transd2l de4);
Lam.pp le4;
Debru.pp (T.transl2d (Lam.reduce (T.transd2l de4)));
Debru.pp (Debru.reduce de4);
print_newline();print_endline ">> transd2l(de5) & le5";
Lam.pp (T.transd2l de5);
Lam.pp le5;
print_newline();print_endline ">> transl2d(reduce(transd2l(de6))) & reduce(de6)";
Lam.pp (T.transd2l de6);
Lam.pp le6;
Debru.pp (T.transl2d (Lam.reduce (T.transd2l de6)));
Debru.pp (Debru.reduce de6);
print_newline();print_endline ">> transl2d(reduce(transd2l(de7))) & reduce(de7)";
Lam.pp (T.transd2l de7);
Lam.pp le7;
Debru.pp (T.transl2d (Lam.reduce (T.transd2l de7)));
Debru.pp (Debru.reduce de7);
print_newline();print_endline ">> transl2d(reduce(transd2l(de8))) & reduce(de8)";
Lam.pp (T.transd2l de8);
Lam.pp le8;
Debru.pp (T.transl2d (Lam.reduce (T.transd2l de8)));
Debru.pp (Debru.reduce de8);
print_newline();print_endline ">> transl2d(reduce(transd2l(de9))) & reduce(de9)";
Lam.pp (T.transd2l de9);
Lam.pp le9;
Debru.pp (T.transl2d (Lam.reduce (T.transd2l de9)));
Debru.pp (Debru.reduce de9))



이번엔 3번 숙제 파일 맨 뒤에 이 내용을 붙인 후

ocaml 6_3.ml
과 같이 한번에 실행합니다. 실행 결과는 아래와 같습니다.
transd2l의 경우 1번과 2번의 reduce가 정확히 작성되어있지 않으면 제대로 테스트 할 수 없습니다. (transd2l은 유일한 결과를 내지 않으니 각자의 구현에 따라 결과가 다를 것입니다)

/**************transl2d test***************/
>> de2=trans(le2) & original de2
L.(L.1 L.0)
L.(L.1 L.0)

>> de4=trans(le4) & original de4
L.L.(L.(L.(0 1) 2) (1 0))
L.L.(L.(L.(0 1) 2) (1 0))

>> de5=trans(le5) & original de5
(L.(0 0) L.(0 0))
(L.(0 0) L.(0 0))

>> de6=trans(le6) & original de6
(L.(L.1 (L.(0 0) L.(0 0))) L.0)
(L.(L.1 (L.(0 0) L.(0 0))) L.0)

>> de7=trans(le7) & original de7
(L.L.L.((1 2) (0 2)) L.0)
(L.L.L.((1 2) (0 2)) L.0)

>> de8=trans(le8) & original de8
(L.L.L.L.(((2 3) (1 3)) (0 3)) L.0)
(L.L.L.L.(((2 3) (1 3)) (0 3)) L.0)

>> de9=trans(le9) & original de9
L.((0 (L.L.L.((1 2) (0 2)) L.0)) L.0)
L.((0 (L.L.L.((1 2) (0 2)) L.0)) L.0)

/**************transd2l test***************/
>> transl2d(reduce(transd2l(de2))) & reduce(de2)
\(a).(\(c).a \(b).b)
\(y).(\(x).y \(z).z)
L.0
L.0

>> transl2d(reduce(transd2l(de4))) & reduce(de4)
\(a).\(b).(\(c).(\(d).(d c) a) (a b))
\(z).\(w).(\(x).(\(y).(y x) z) (z w))
L.L.(1 (1 0))
L.L.(1 (1 0))

>> transd2l(de5) & le5
(\(b).(b b) \(a).(a a))
(\(x).(x x) \(y).(y y))

>> transl2d(reduce(transd2l(de6))) & reduce(de6)
(\(b).(\(e).b (\(d).(d d) \(c).(c c))) \(a).a)
(\(w).(\(z).w (\(x).(x x) \(y).(y y))) \(a).a)
L.0
L.0

>> transl2d(reduce(transd2l(de7))) & reduce(de7)
(\(b).\(c).\(d).((c b) (d b)) \(a).a)
(\(x).\(a).\(b).((a x) (b x)) \(y).y)
L.L.((1 L.0) (0 L.0))
L.L.((1 L.0) (0 L.0))

>> transl2d(reduce(transd2l(de8))) & reduce(de8)
(\(b).\(c).\(d).\(e).(((c b) (d b)) (e b)) \(a).a)
(\(x).\(a).\(b).\(c).(((a x) (b x)) (c x)) \(y).y)
L.L.L.(((2 L.0) (1 L.0)) (0 L.0))
L.L.L.(((2 L.0) (1 L.0)) (0 L.0))

>> transl2d(reduce(transd2l(de9))) & reduce(de9)
\(a).((a (\(d).\(e).\(f).((e d) (f d)) \(c).c)) \(b).b)
\(c).((c (\(x).\(a).\(b).((a x) (b x)) \(y).y)) \(y').y')
L.((0 L.L.((1 L.0) (0 L.0))) L.0)
L.((0 L.L.((1 L.0) (0 L.0))) L.0)
_________________
TA

[임창원]

언제나 감사드려요 ㅎㅎ