SKI, true as K

pcp/lambda.hs

@@ -154,6 +154,10 @@ ttran (App x y) = App (ttran x) (ttran y)
 ttran (Abs x (Var y)) =
     if x == y then I
     else App K (Var y)
+-- translate \xy.x to K not to S (K K) I
+ttran (Abs x (Abs y (Var z))) =
+    if x == z then K else
+    App K (ttran (Abs y (Var z)))
 ttran (Abs x (Abs y e1)) =
     let f = elem x (fvs e1) in
     if f then ttran (Abs x (ttran (Abs y e1)))
@@ -166,19 +170,71 @@ ttran (Abs x (App e1 e2)) =
 ttran (Abs x ski) = App K (ttran ski)
 ttran x   = x
 
-
-
 true :: Term
 true = Abs "x" (Abs "y" (Var "x"))
 
 false :: Term
 false = Abs "x" (Abs "y" (Var "y"))
 
-ite :: Term
+at = Abs "x" true
+af = Abs "x" false
+
 ite = Abs "c" (Abs "a" (Abs "b" (App (App (Var "c") (Var "a")) (Var "b"))))
 
-land :: Term
 land = Abs "x" (Abs "y" (App (App (Var "x") (Var "y")) false))
 
-lor :: Term
 lor = Abs "x" (Abs "y" (App (App (Var "x") true) (Var "y")))
+
+pair = Abs "a" (Abs "b" (Abs "c" (App (App (Var "c") (Var "a")) (Var "b"))))
+
+first = Abs "p" (App (Var "p") true)
+second = Abs "p" (App (Var "p") false)
+ycomb = Abs "f" (App (Abs "x" (App (Var "f") (App (Var "x") (Var "x")))) (Abs "x" (App (Var "f") (App (Var "x") (Var "x")))))
+
+empty = Abs "a" (Abs "b" (Abs "x" (Var "x")))
+a = Abs "a" (Abs "b" (Abs "x" (App (Var "a") (Var "x"))))
+b = Abs "a" (Abs "b" (Abs "x" (App (Var "b") (Var "x"))))
+ab = Abs "a" (Abs "b" (Abs "x" (App (Var "a") (App (Var "b") (Var "x")))))
+bba = Abs "a" (Abs "b" (Abs "x" (App (Var "b") (App (Var "b") (App (Var "a") (Var "x"))))))
+isempty = Abs "s" (App (App (App (Var "s") af) af) true)
+conc = Abs "y" (Abs "z" (Abs "a" (Abs "b" (Abs "x" (App (App (App (Var "y") (Var "a")) (Var "b")) (App (App (App (Var "z") (Var "a")) (Var "b")) (Var "x")))))))
+
+prep_a = Abs "s" (Abs "a" (Abs "b" (Abs "x" (App (Var "a") (App (App (App (Var "s") (Var "a")) (Var "b")) (Var "x"))))))
+
+prep_b = Abs "s" (Abs "a" (Abs "b" (Abs "x" (App (Var "b") (App (App (App (Var "s") (Var "a")) (Var "b")) (Var "x"))))))
+
+hd_a = Abs "s" (App (App (App (Var "s") at) af) false)
+hd_b = Abs "s" (App (App (App (Var "s") af) at) false)
+hd_eq = Abs "x" (Abs "y" (App (App lor (App (App land (App hd_a (Var "x"))) (App hd_a (Var "y")))) (App (App land (App hd_b (Var "x"))) (App hd_b (Var "y")))))
+
+next_a = Abs "x" (App (App pair (App prep_a (App first (Var "x")))) (App first (Var "x")))
+next_b = Abs "x" (App (App pair (App prep_b (App first (Var "x")))) (App first (Var "x")))
+
+tl_str = Abs "s" (App second (App (App (App (Var "s") next_a) next_b) (App (App pair empty) empty)))
+
+eq = App ycomb (Abs "f" (Abs "x" (Abs "y" (App (App (App ite (App (App lor (App isempty (Var "x"))) (App isempty (Var "y")))) (App (App land (App isempty (Var "x"))) (App isempty (Var "y")))) (App (App land (App (App hd_eq (Var "x")) (Var "y"))) (App (App (Var "f") (App tl_str (Var "x"))) (App tl_str (Var "y"))))))))
+
+prefix = App ycomb (Abs "f" (Abs "x" (Abs "y" (App  (App (App ite (App isempty (Var "x"))) true) (App (App land (App (App hd_eq (Var "x")) (Var "y"))) (App (App (Var "f") (App tl_str (Var "x"))) (App tl_str (Var "y"))))))))
+
+nil = Abs "c" (Abs "n" (Var "n"))
+cons = Abs "h" (Abs "t" (Abs "c" (Abs "n" (App (App (Var "c") (Var "h")) (App (App (Var "t") (Var "c")) (Var "n"))))))
+is_nil = Abs "l" (App (App (Var "l") (Abs "h" (Abs "t" false))) true)
+
+hd_l = Abs "l" (App (App (App (Var "l") (Abs "h" (Abs "t" (Abs "u" (Var "h"))))) (Abs "u" (App ycomb (Abs "x" (Var "x"))))) nil)
+
+next_l = Abs "x" (Abs "p" (App (App pair (App (App cons (Var "x")) (App first (Var "x")))) (App first (Var "p"))))
+
+tl_l = Abs "l" (App second (App (App (Var "l") next_l) (App (App pair nil) nil)))
+
+append = Abs "x" (Abs "y" (Abs "c" (Abs "n" (App (App (Var "x") (Var "c")) (App (App (Var "y") (Var "c")) (Var "n"))))))
+
+p1 = App (App pair bba) b
+p2 = App (App pair b) ab
+p3 = App (App pair a) bba
+pairs = App (App cons p1) (App (App cons p2) (App (App cons p3) nil))
+
+simp = Abs "p" (App (App (App ycomb (Abs "f" (Abs "x" (Abs "y" (App  (App (App ite (App (App lor (App isempty (Var "x"))) (App isempty (Var "y")))) (App (App pair (Var "x")) (Var "y"))) (App (App (Var "f") (App tl_str (Var "x"))) (App tl_str (Var "y")))))))) (App first (Var "p"))) (App second (Var "p")))
+
+pvalid = Abs "p" (App (App lor (App (App prefix (App first (Var "p"))) (App second (Var "p")))) (App (App prefix (App second (Var "p"))) (App first (Var "p"))))
+
+find_eq = App ycomb ()