Skip to content

Instantly share code, notes, and snippets.

@krtx
Last active May 24, 2018 02:10
Show Gist options
  • Save krtx/6dd955744ccad33e47082eb19d302e7a to your computer and use it in GitHub Desktop.
Save krtx/6dd955744ccad33e47082eb19d302e7a to your computer and use it in GitHub Desktop.
(* 演繹(論理式列)をツリーで表現する型 *)
type prop =
| Arg of int (* i番目の前提 *)
| App of prop * prop (* MP *)
| Axm of string (* 公理 *)
(* 演繹定理の(⇐)に相当する*)
let rec reduce_one = function
| Arg x ->
if x = 0
then App (App (Axm "s", Axm "k"), Axm "k") (* 3) に相当 *)
else App (Axm "k", Arg (x - 1)) (* 2) に相当 *)
| App (p1, p2) -> App (App (Axm "s", reduce_one p1), reduce_one p2) (* 4) に相当 *)
| Axm a -> App (Axm "k", Axm a) (* 1) に相当 *)
(* 前提がなくなるまで演繹定理の(⇐)を適用する *)
let rec reduce prop = function
| 0 -> prop
| n -> reduce (reduce_one prop) (n - 1)
let rec to_string = function
| Arg x -> Format.sprintf "v#%d" x
| App (p1, p2) ->
begin
match p2 with
| App _ -> Format.sprintf "%s (%s)" (to_string p1) (to_string p2)
| _ -> Format.sprintf "%s %s" (to_string p1) (to_string p2)
end
| Axm s -> s
let s : ('a -> 'b -> 'c) -> (('a -> 'b) -> ('a -> 'c)) = fun x y z -> x z (y z)
let k : 'a -> 'b -> 'a = fun x y -> x
(* reduce (App (App (Arg 2, Arg 0), Arg 1)) 3 |> to_string *)
let b : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c) = s (s (k s) (s (s (k s) (s (k k) (k s))) (s (s (k s) (s (k k) (k k))) (s (k k) (s k k))))) (s (s (k s) (s (s (k s) (s (k k) (k s))) (s (s (k s) (s (k k) (k k))) (s (s (k s) (k k)) (k k))))) (s (s (k s) (s (s (k s) (s (k k) (k s))) (s (k k) (k k)))) (s (k k) (k k))))
(* reduce (App (Arg 2, App (Arg 1, Arg 0))) 3 |> to_string *)
let c : ('a -> 'b -> 'c) -> ('b -> 'a -> 'c) = s (s (k s) (s (s (k s) (s (k k) (k s))) (s (s (k s) (s (s (k s) (s (k k) (k s))) (s (s (k s) (s (k k) (k k))) (s (k k) (s k k))))) (s (s (k s) (s (s (k s) (s (k k) (k s))) (s (k k) (k k)))) (s (k k) (k k)))))) (s (s (k s) (s (k k) (k k))) (s (s (k s) (k k)) (k k)))
(* reduce (App (App (Arg 1, Arg 0), Arg 0)) 2 |> to_string *)
let w : ('a -> 'a -> 'b) -> ('a -> 'b) = s (s (k s) (s (s (k s) (s (k k) (s k k))) (s (s (k s) (k k)) (k k)))) (s (s (k s) (k k)) (k k))
(* reduce (App (Arg 1, App (Arg 2, Arg 0))) 3 |> to_string *)
let b' : ('a -> 'b) -> ('b -> 'c) -> ('a -> 'c) = s (s (k s) (s (s (k s) (s (k k) (k s))) (s (s (k s) (s (k k) (k k))) (s (s (k s) (k k)) (k k))))) (s (s (k s) (s (s (k s) (s (k k) (k s))) (s (s (k s) (s (k k) (k k))) (s (k k) (s k k))))) (s (s (k s) (s (s (k s) (s (k k) (k s))) (s (k k) (k k)))) (s (k k) (k k))))
(* reduce (App (Arg 0, Arg 1)) 2 |> to_string *)
let c_star : 'a -> ('a -> 'b) -> 'b = s (s (k s) (s (s (k s) (k k)) (k k))) (s (k k) (s k k))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment