From 2c5bd04e187034aedb9f31a6dbdba6c69ad6197a Mon Sep 17 00:00:00 2001 From: Xuan Date: Sun, 19 Sep 2021 13:58:43 -0400 Subject: [PATCH] Add note on extended unification to README, increase version number. --- Project.toml | 2 +- README.md | 27 +++++++++++++++++---------- test/unify.jl | 2 +- 3 files changed, 19 insertions(+), 12 deletions(-) diff --git a/Project.toml b/Project.toml index b896ade..c05aeab 100644 --- a/Project.toml +++ b/Project.toml @@ -1,7 +1,7 @@ name = "Julog" uuid = "5d8bcb5e-2b2c-4a96-a2b1-d40b3d3c344f" authors = ["Xuan "] -version = "0.1.10" +version = "0.1.11" [compat] julia = "1.0" diff --git a/README.md b/README.md index ea7e393..37cdb22 100644 --- a/README.md +++ b/README.md @@ -182,6 +182,20 @@ funcs[:lookup] = Dict((:foo,) => "hello", (:bar,) => "world") See [`test/custom_funcs.jl`](test/custom_funcs.jl) for more examples. +Unlike Prolog, Julog also supports [extended unification](https://www.sciencedirect.com/science/article/pii/0743106687900021) via the evaluation of functional terms. In other words, the following terms unify: +```julia +julia> unify(@julog(f(X, X*Y, Y)), @julog(f(4, 20, 5))) +Dict{Var, Term} with 2 entries: + Y => 5 + X => 4 +``` + +However, the extent of such unification is limited. If variables used within a functional expression are not sufficiently instantiated at the time of evaluation, evaluation will be partial, causing unification to fail: +```julia +julia> unify(@julog(f(X, X*Y, Y)), @julog(f(X, 20, 5))) === nothing +true +``` + ## Built-in Predicates `Julog` provides a number of built-in predicates for control-flow and convenience. Some of these are also part of ISO Prolog, but may not share the exact same behavior. @@ -205,8 +219,7 @@ See [`test/builtins.jl`](test/builtins.jl) for usage examples. ## Conversion Utilities -Julog provides some support for converting and manipulating logical formulae, -for example, conversion to negation, conjunctive, or disjunctive normal form: +Julog provides some support for converting and manipulating logical formulae, for example, conversion to negation, conjunctive, or disjunctive normal form: ```julia julia> formula = @julog and(not(and(a, not(b))), c) julia> to_nnf(formula) @@ -217,17 +230,11 @@ julia> to_dnf(formula) or(and(not(a), c), and(b, c)) ``` -This can be useful for downstream applications, such as classical planning. -Note however that these conversions do not handle the implicit existential -quantification in Prolog semantics, and hence are not guaranteed to preserve equivalence when free variables are involved. In particular, care should be -taken with negations of conjunctions of unbound predicates. For example, -the following expression states that "All ravens are black.": +This can be useful for downstream applications, such as classical planning. Note however that these conversions do not handle the implicit existential quantification in Prolog semantics, and hence are not guaranteed to preserve equivalence when free variables are involved. In particular, care should be taken with negations of conjunctions of unbound predicates. For example, the following expression states that "All ravens are black.": ```julia @julog not(and(raven(X), not(black(X)))) ``` -However, `to_dnf` doesn't handle the implied existential quantifier over `X`, -and gives the non-equivalent statement "Either there are no ravens, or there -exist black things, or both.": +However, `to_dnf` doesn't handle the implied existential quantifier over `X`, and gives the non-equivalent statement "Either there are no ravens, or there exist black things, or both.": ```julia @julog or(and(not(raven(X))), and(black(X))) ``` diff --git a/test/unify.jl b/test/unify.jl index d3428cc..7679b32 100644 --- a/test/unify.jl +++ b/test/unify.jl @@ -8,7 +8,7 @@ subst = unify(@julog(f(g(X, h(X, b)), Z)), @julog(f(g(a, Z), Y))) @test unify(@julog(A), @julog(functor(A)), false) == @varsub {A => functor(A)} @test unify(@julog(A), @julog(functor(A)), true) === nothing -# Test semantic unification of arithmetic functions (Prolog can't do this!) +# Test extended unification of arithmetic functions (Prolog can't do this!) # X unifies to 4, Y unifies to 5, so *(X, Y) unifies by evaluation to 20 @test unify(@julog(f(X, X*Y, Y)), @julog(f(4, 20, 5))) == @varsub {Y => 5, X => 4} # X unifies to 4, Y unifies to /(20,4), so *(X, Y) unifies by evaluation to 20