Skip to content

Instantly share code, notes, and snippets.

@nyuichi
Last active April 6, 2019 11:54
Show Gist options
  • Save nyuichi/3e596063f62cba352e6041c3a91b213f to your computer and use it in GitHub Desktop.
Save nyuichi/3e596063f62cba352e6041c3a91b213f to your computer and use it in GitHub Desktop.
; -*- mode: scheme;-*-
; Implementation of resolution principle for first-order logic in Egison
(define $unordered-pair
(lambda [$m]
(matcher
{[<pair $ $> [m m] {[[$x $y] {[x y] [y x]}]}]
[$ [something] {[$tgt {tgt}]}]})))
(define $positive?
(lambda $x (gt? x 0)))
(define $term
(algebraic-data-matcher
{<var integer> <compound string (list term)>}))
(define $app
(cambda $xs
(match xs (list something)
{[<cons $x $xs>
<Compound x xs>]})))
(define $var
(lambda $n
<Var n>))
(define $x 0)
(define $y 1)
(define $z 2)
(define $w 3)
(define $t1 (app "P" (app "g" (var x)) (var y)))
(define $t2 (app "P" (app "g" (app "g" (app "c"))) (app "c")))
(define $occur
(pattern-function [$v]
(| <var v>
<compound _ <join _ <cons (occur v) _>>>)))
(define $test-occur
(lambda [$v $t]
(match t term
{[(occur ,v) #t]
[_ #f]})))
(assert "occur1"
(test-occur x t1))
(assert "occur2"
(not (test-occur z t1)))
(define $fv
(match-all-lambda term
{[(occur $v) v]}))
(assert "fv1"
(match (fv t1) (multiset something)
{[,{0 1} #t]
[_ #f]}))
(assert-equal "fv2"
(fv t2)
{})
(define $subst
(match-lambda [something term]
{[[$u <var $n>]
(match u (multiset [integer term])
{[<cons [,n $t] _> t]
[_ <Var n>]})]
[[$u <compound $f $xs>]
<Compound f (map (lambda $x (subst u x)) xs)>]}))
(assert-equal "subst1"
(subst {[y <Var x>] [x <Var z>]} t1)
<Compound "P" {<Compound "g" {<Var 2>}> <Var 0>}>)
(assert-equal "subst2"
(subst {[z <Var z>]} t1)
<Compound "P" {<Compound "g" {<Var 0>}> <Var 1>}>)
(define $unify
(match-lambda (unordered-pair term)
{[<pair <var $n> <var ,n>>
{}]
[<pair <var $n> (& $t !(occur ,n))>
{[n t]}]
[<pair <compound $f <nil>> <compound ,f <nil>>>
{}]
[<pair <compound $f <cons $x $xs>> <compound ,f <cons $y $ys>>>
(match (unify x y) eq
{[,#f #f]
[$u1 (match (unify (subst u1 <Compound f xs>) (subst u1 <Compound f ys>)) eq
{[,#f #f]
[$u2 {@u1 @u2}]})]})]
[_ #f]}))
(assert-equal "unify1"
(unify (var x) (var x))
{})
(assert-equal "unify2"
(unify t1 (var z))
{[z t1]})
(assert-equal "unify3"
(unify t1 t2)
{[0 <Compound "g" {<Compound "c" {}>}>] [1 <Compound "c" {}>]})
(assert-equal "unify4"
(unify (var x) t1)
#f)
(define $literal
(algebraic-data-matcher
{<lit integer term>}))
(define $fv-clause
(match-all-lambda (multiset literal)
{[<cons <lit _ (occur $v)> _> v]}))
(define $subst-clause
(match-all-lambda [something (multiset literal)]
{[[$u <cons <lit $p $t> _>]
<Lit p (subst u t)>]}))
(define $unifiable?
(lambda $t
(lambda $s
(collection? (unify t s)))))
(define $resolution
(match-all-lambda (multiset (multiset literal))
{[<cons <cons <lit (& ?positive? $p) $t> $xs>
<cons <cons <lit ,(neg p) (& ?(unifiable? t) $s)> $ys>
_>>
(let {[$u (unify t s)]}
{@(subst-clause u xs) @(subst-clause u ys)})]}))
(define $rename-problem
(match-lambda [integer (list (list literal))]
{[[$n <nil>]
{}]
[[$n <cons $c $cs>]
(let {[$u (zip (fv-clause c) (map (lambda $x <Var x>) (from n)))]}
(cons (subst-clause u c)
(rename-problem (+ n (length u)) cs)))]}))
(define $solve
(match-lambda (multiset (multiset literal))
{[<cons <nil> _>
<REFUTE>]
[$p
(let {[$q (resolution (rename-problem 0 p))]}
(if (include?/m (multiset literal) p q)
<SATURATED>
(solve {@p @q})))]}))
(define $t3 (app "P" (var x) (app "f" (var x) (var y))))
(define $t4 (app "P" (app "c") (var y)))
; 1. Problem:
; (\forall x y. \exists z. P(g(x),y) \to P(x,z)) \land (\forall y. \lnot P(c,y)) \land P(g(g(c)),c)
; 2. Prenex normal form
; \forall x y. \exists z. (P(g(x),y) \to P(x,z)) \land \lnot P(c,y) \land P(g(g(c)),c)
; 3. Skolemization
; \forall x y. (P(g(x),y) \to P(x,f(x,y))) \land \lnot P(c,y) \land P(g(g(c)),c)
; 4. Conjunction normal form
; (\lnot P(g(x),y) \lor P(x,f(x,y))) \land \lnot P(c,y) \land P(g(g(c)),c)
(define $p1 {{<Lit -1 t1> <Lit 1 t3>} {<Lit -1 t4>} {<Lit 1 t2>}})
(assert-equal "solve1"
(solve p1)
<REFUTE>)
; Drinker's paradox
; 1. \lnot \exists x. D(x) \to \forall y. D(y)
; 2. \forall x. \exists y. D(x) \land \lnot D(y)
; 3. \forall x. D(x) \land \lnot D(c)
; 4. D(x) \land \lnot D(c)
(define $p2
{{<Lit 1 (app "D" (var x))>} {<Lit -1 (app "D" (app "c"))>}})
(assert-equal "solve2"
(solve p2)
<REFUTE>)
; Recall the axioms of groups:
; (1) (x*y)*z = x*(y*z)
; (2) x*(x^-1)= 1
; (3) (x^-1)*x = 1
; (4) x*1 = x
; (5) 1*x = x
; It is known that (3) and (5) above are redundant, i.e., provable from other axioms. Let's prove this!
(define $eql (lambda [$x $y] (app "=" x y)))
(define $p (lambda [$x $y] (app "p" x y)))
(define $i (lambda $x (app "i" x)))
(define $e (app "e"))
(define $e1 (app "e1"))
(define $e2 (app "e2"))
; (a) axioms of groups
; - p(p(x,y),z) = p(x,p(y,z))
; - p(x,i(x)) = e
; - p(x,e) = x
; (b) axioms of equality
; - x = x
; - \lnot (x = y) \lor (y = x)
; - \lnot (x = y) \lor lnot (y = z) \lor (x = z)
; - \lnot (x = y) \lnot (z = w) \lor (p(x,z) = p(y,w))
; - \lnot (x = y) \lor (i(x) = i(y))
; (c) (negation) of the goal
; - \lnot (p(i(e1),e1) = e) \lor \lnot (p(e,e2) = e2)
; (1) (2) (4) |= (5)
(define $p3
{{<Lit 1 (eql (p (p (var x) (var y)) (var z)) (p (var x) (p (var y) (var z))))>}
{<Lit 1 (eql (p (var x) (i (var x))) e)>}
{<Lit 1 (eql (p (var x) e) (var x))>}
{<Lit 1 (eql (var x) (var x))>}
{<Lit -1 (eql (var x) (var y))> <Lit 1 (eql (var y) (var x))>}
{<Lit -1 (eql (var x) (var y))> <Lit -1 (eql (var y) (var z))> <Lit 1 (eql (var x) (var z))>}
{<Lit -1 (eql (var x) (var y))> <Lit -1 (eql (var z) (var w))> <Lit 1 (eql (p (var x) (var z)) (p (var y) (var w)))>}
{<Lit -1 (eql (var x) (var y))> <Lit 1 (eql (i (var x)) (i (var y)))>}
{<Lit -1 (eql (p e e1) e1)>}})
(assert-equal "solve3"
(solve p3)
<REFUTE>)
; (1) (2) (4) |= (3)
(define $p4
{{<Lit 1 (eql (p (p (var x) (var y)) (var z)) (p (var x) (p (var y) (var z))))>}
{<Lit 1 (eql (p (var x) (i (var x))) e)>}
{<Lit 1 (eql (p (var x) e) (var x))>}
{<Lit 1 (eql (var x) (var x))>}
{<Lit -1 (eql (var x) (var y))> <Lit 1 (eql (var y) (var x))>}
{<Lit -1 (eql (var x) (var y))> <Lit -1 (eql (var y) (var z))> <Lit 1 (eql (var x) (var z))>}
{<Lit -1 (eql (var x) (var y))> <Lit -1 (eql (var z) (var w))> <Lit 1 (eql (p (var x) (var z)) (p (var y) (var w)))>}
{<Lit -1 (eql (var x) (var y))> <Lit 1 (eql (i (var x)) (i (var y)))>}
{<Lit -1 (eql (p (i e2) e2) e)>}})
(assert-equal "solve4"
(solve p4)
<REFUTE>)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment