sk.ml

(* 演繹(論理式列)をツリーで表現する型 *)
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))