diff --git a/FicroKanSharp.Test/Arithmetic.fs b/FicroKanSharp.Test/Arithmetic.fs new file mode 100644 index 0000000..8c42c98 --- /dev/null +++ b/FicroKanSharp.Test/Arithmetic.fs @@ -0,0 +1,89 @@ +namespace FicroKanSharp.Test + +open FicroKanSharp +open FsUnitTyped +open Xunit + +module Arithmetic = + + type Nat = Nat + + [] + let ``Arithmetic example`` () = + let zero : Term = Term.Symbol ("zero", []) + + let succ (x : Term) : Term = + Term.Symbol ("succ", [ TypedTerm.make x ]) + + let rec ofInt (n : int) : Term = + if n = 0 then + zero + else + succ (ofInt (n - 1)) + + // "pluso x y z" is "x + y == z". + let rec pluso (x : Term) (y : Term) (z : Term) : Goal = + let succCase = + Goal.callFresh (fun n -> + let n = Term.Variable n + + Goal.callFresh (fun m -> + let m = Term.Variable m + + Goal.conj + (Goal.equiv x (succ n)) + (Goal.conj (Goal.equiv z (succ m)) (Goal.delay (fun () -> pluso n y m))) + ) + ) + + let zeroCase = + Goal.conj (Goal.equiv x zero) (Goal.equiv y z) + + Goal.disj zeroCase succCase + + Goal.evaluate (Goal.callFresh (fun z -> Goal.equiv (Term.Variable z) (Term.Variable z))) State.empty + |> Stream.toList + |> shouldEqual [ Map.empty ] + + // Evaluate 1 + 1 + Goal.evaluate (Goal.callFresh (fun z -> pluso (ofInt 1) (ofInt 1) (Term.Variable z))) State.empty + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, TypedTerm.make (succ (Term.Variable (VariableCount 2))) + VariableCount 1, TypedTerm.make (ofInt 0) + VariableCount 2, TypedTerm.make (ofInt 1) + ] + ) + + // Evaluate 2 + 2 + Goal.evaluate (Goal.callFresh (fun z -> pluso (ofInt 2) (ofInt 2) (Term.Variable z))) State.empty + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, TypedTerm.make (succ (Term.Variable (VariableCount 2))) + VariableCount 1, TypedTerm.make (ofInt 1) + VariableCount 2, TypedTerm.make (succ (Term.Variable (VariableCount 4))) + VariableCount 3, TypedTerm.make zero + VariableCount 4, TypedTerm.make (ofInt 2) + ] + ) + + // Find n such that n + n = 4 + Goal.evaluate (Goal.callFresh (fun z -> pluso (Term.Variable z) (Term.Variable z) (ofInt 4))) State.empty + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, TypedTerm.make (succ (Term.Variable (VariableCount 1))) + VariableCount 1, TypedTerm.make (succ (Term.Variable (VariableCount 3))) + VariableCount 2, TypedTerm.make (ofInt 3) + VariableCount 3, TypedTerm.make zero + VariableCount 4, TypedTerm.make (ofInt 2) + ] + ) diff --git a/FicroKanSharp.Test/FicroKanSharp.Test.fsproj b/FicroKanSharp.Test/FicroKanSharp.Test.fsproj index de76e7c..aeeefe5 100644 --- a/FicroKanSharp.Test/FicroKanSharp.Test.fsproj +++ b/FicroKanSharp.Test/FicroKanSharp.Test.fsproj @@ -6,6 +6,7 @@ + diff --git a/FicroKanSharp/Domain.fs b/FicroKanSharp/Domain.fs index 543a7f1..e4b9f6c 100644 --- a/FicroKanSharp/Domain.fs +++ b/FicroKanSharp/Domain.fs @@ -9,6 +9,85 @@ module private Variable = type Term<'a> = | Literal of 'a | Variable of Variable + | Symbol of name : string * args : TypedTerm list + + override this.ToString () = + match this with + | Symbol (name, args) -> + let s = + args + |> List.map (sprintf "%O") + |> String.concat ", " + + $"{name}[{s}]" + | Variable (VariableCount v) -> $"x{v}" + | Literal t -> t.ToString () + +and internal TermEvaluator<'ret> = + abstract Eval<'a when 'a : equality> : 'a Term -> 'ret + +and internal TermCrate = + abstract Apply<'ret> : TermEvaluator<'ret> -> 'ret + +and [] TypedTerm = + internal + | TypedTerm of TermCrate + + override this.Equals (other : obj) : bool = + match this with + | TypedTerm tc -> + + match other with + | :? TypedTerm as other -> + match other with + | TypedTerm other -> tc.Equals other + | _ -> false + + override this.GetHashCode () = + match this with + | TypedTerm tc -> + { new TermEvaluator<_> with + override _.Eval t = t.GetHashCode () + } + |> tc.Apply + + override this.ToString () = + match this with + | TypedTerm tc -> tc.ToString () + +[] +module internal TermCrate = + let make<'a when 'a : equality> (t1 : 'a Term) = + { new obj() with + override this.ToString () = t1.ToString () + + override this.Equals other = + match other with + | :? TermCrate as other -> + { new TermEvaluator<_> with + member _.Eval<'b when 'b : equality> (other : 'b Term) = + if typeof<'a> = typeof<'b> then + t1 = unbox other + else + + printfn "%+A, %+A" typeof<'a> typeof<'b> + false + } + |> other.Apply + | _ -> false + interface TermCrate with + member _.Apply eval = eval.Eval t1 + } + +[] +module TypedTerm = + let force<'a> (TypedTerm t) : 'a Term = + { new TermEvaluator<_> with + member _.Eval t = unbox t + } + |> t.Apply + + let make<'a when 'a : equality> (t : 'a Term) : TypedTerm = TermCrate.make t |> TypedTerm /// Equality constraint is required because we use this crate for unification type internal TermPairEvaluator<'ret> = @@ -24,29 +103,6 @@ module internal TermPairCrate = member _.Apply eval = eval.Eval t1 t2 } -type internal TermEvaluator<'ret> = - abstract Eval<'a> : 'a Term -> 'ret - -type internal TermCrate = - abstract Apply<'ret> : TermEvaluator<'ret> -> 'ret - -[] -module internal TermCrate = - let make<'a> (t1 : 'a Term) = - { new TermCrate with - member _.Apply eval = eval.Eval t1 - } - -type TypedTerm = internal TypedTerm of TermCrate - -[] -module TypedTerm = - let force<'a> (TypedTerm t) : 'a Term = - { new TermEvaluator<_> with - member _.Eval t = unbox t - } - |> t.Apply - type Goal = private | Equiv of TermPairCrate diff --git a/FicroKanSharp/Goal.fs b/FicroKanSharp/Goal.fs index 8ae3d7b..4336377 100644 --- a/FicroKanSharp/Goal.fs +++ b/FicroKanSharp/Goal.fs @@ -7,14 +7,16 @@ module Goal = let delay g = Goal.Delay g + /// Boolean "or": either goal must be satisfied. let disj (goal1 : Goal) (goal2 : Goal) : Goal = Goal.Disj (goal1, goal2) + /// Boolean "and": both goals must be satisfied simultaneously. let conj (goal1 : Goal) (goal2 : Goal) : Goal = Goal.Conj (goal1, goal2) let equiv<'a when 'a : equality> (term1 : 'a Term) (term2 : 'a Term) : Goal = TermPairCrate.make term1 term2 |> Goal.Equiv - let walk<'a> (u : Term<'a>) (s : State) : Term<'a> = + let private walk<'a> (u : Term<'a>) (s : State) : Term<'a> = match u with | Term.Variable u -> match Map.tryFind u s.Substitution with @@ -26,12 +28,12 @@ module Goal = |> subst.Apply | u -> u - let extend<'a> (v : Variable) (t : Term<'a>) (s : State) = + let private extend<'a when 'a : equality> (v : Variable) (t : Term<'a>) (s : State) = { s with Substitution = Map.add v (TermCrate.make t |> TypedTerm) s.Substitution } - let rec unify<'a when 'a : equality> (u : 'a Term) (v : 'a Term) (s : State) : State option = + let rec private unify<'a when 'a : equality> (u : 'a Term) (v : 'a Term) (s : State) : State option = let u = walk u s let v = walk v s @@ -40,6 +42,35 @@ module Goal = | Term.Variable u, v -> extend u v s |> Some | u, Term.Variable v -> extend v u s |> Some | Term.Literal u, Term.Literal v -> if u = v then Some s else None + | Term.Symbol (name1, args1), Term.Symbol (name2, args2) -> + if (name1 <> name2) || (args1.Length <> args2.Length) then + None + else + + let rec go state args1 args2 = + match args1, args2 with + | [], [] -> Some state + | _, [] + | [], _ -> None + | TypedTerm arg1 :: args1, TypedTerm arg2 :: args2 -> + { new TermEvaluator<_> with + member _.Eval<'t when 't : equality> (arg1 : Term<'t>) = + { new TermEvaluator<_> with + member _.Eval<'u when 'u : equality> (arg2 : Term<'u>) = + if typeof<'t> = typeof<'u> then + match unify arg1 (arg2 |> unbox) state with + | None -> None + | Some s -> go s args1 args2 + else + None + } + |> arg2.Apply + } + |> arg1.Apply + + go s args1 args2 + + | _, _ -> None let rec evaluate (goal : Goal) (state : State) : Stream = match goal with @@ -47,8 +78,8 @@ module Goal = { new TermPairEvaluator<_> with member _.Eval u v = match unify u v state with - | None -> Stream.mzero - | Some unification -> Stream.Nonempty (unification, Stream.mzero) + | None -> Stream.empty + | Some unification -> Stream.Nonempty (unification, Stream.empty) } |> pair.Apply | Goal.Fresh goal -> @@ -59,6 +90,36 @@ module Goal = { state with VariableCounter = Variable.incr state.VariableCounter } - | Goal.Disj (goal1, goal2) -> Stream.mplus (evaluate goal1 state) (evaluate goal2 state) + | Goal.Disj (goal1, goal2) -> Stream.union (evaluate goal1 state) (evaluate goal2 state) | Goal.Conj (goal1, goal2) -> Stream.bind (evaluate goal1 state) (evaluate goal2) | Goal.Delay g -> Stream.Procedure (fun () -> evaluate (g ()) state) + +(* + (dene (mK-reify s/c* ) +(map reify-state/1st-var s/c* )) +(dene (reify-state/1st -var s/c) +(let ((v (walk* (var 0) (car s/c)))) +(walk* v (reify-s v ' ())))) +The reier here, mK-reify, reies a list of states s/c* +by reifying each state's substitution with respect to the rst +variable. The reify-s, reify-name, and walk* helpers are +required for reify-state/1st-var. +(dene (reify-s v s) +(let ((v (walk v s))) +(cond +((var? v) +(let ((n (reify-name (length s)))) +(cons `(, v . , n) s))) +((pair? v) (reify-s (cdr v) (reify-s (car v) s))) +(else s)))) +(dene (reify-name n) +(stringsymbol +(string - append "_" "." (numberstring n)))) +(dene (walk* v s) +(let ((v (walk v s))) +(cond +((var? v) v) +((pair? v) (cons (walk* (car v) s) +(walk* (cdr v) s))) +(else v)))) +*) diff --git a/FicroKanSharp/Stream.fs b/FicroKanSharp/Stream.fs index 65015dc..3613e38 100644 --- a/FicroKanSharp/Stream.fs +++ b/FicroKanSharp/Stream.fs @@ -3,22 +3,34 @@ namespace FicroKanSharp [] [] module Stream = - let mzero : Stream = Stream.Empty + /// This is called mzero in the microKanren paper. + let empty : Stream = Stream.Empty - let rec mplus (s1 : Stream) (s2 : Stream) : Stream = + /// This is called mplus in the microKanren paper. + let rec union (s1 : Stream) (s2 : Stream) : Stream = match s1 with | Stream.Empty -> s2 - | Stream.Procedure s -> Stream.Procedure (fun () -> mplus s2 (s ())) - | Stream.Nonempty (fst, rest) -> Stream.Nonempty (fst, mplus rest s2) + | Stream.Procedure s -> Stream.Procedure (fun () -> union s2 (s ())) + | Stream.Nonempty (fst, rest) -> Stream.Nonempty (fst, union rest s2) - let rec bind (s : Stream) (g : State -> Stream) = + let rec bind (s : Stream) (g : State -> Stream) : Stream = match s with - | Stream.Empty -> mzero + | Stream.Empty -> empty | Stream.Procedure s -> Stream.Procedure (fun () -> bind (s ()) g) - | Stream.Nonempty (fst, rest) -> mplus (g fst) (bind rest g) + | Stream.Nonempty (fst, rest) -> union (g fst) (bind rest g) let rec peel (s : Stream) : (Map * Stream) option = match s with | Stream.Empty -> None | Stream.Nonempty (fst, rest) -> Some (fst.Substitution, rest) | Stream.Procedure p -> peel (p ()) + + /// This will stack-overflow for an infinite stream. + let toList (s : Stream) : Map list = + let rec go acc s = + match s with + | Stream.Empty -> acc + | Stream.Nonempty (fst, rest) -> go (fst.Substitution :: acc) rest + | Stream.Procedure p -> go acc (p ()) + + go [] s |> List.rev