Unification algorithms

[kp]

After an "odyssey" of trying to embed some logic systems into Pure in
order to use their unification capabilities I came to the conclusion
that the best way is - at least for me - to use a "Pure" implementation
of a rule based algorithm.

The Prolog engines (if embedded) may be rather slow and the powerful
systems like 'ciao or 'XSB have "mangled" libraries. The best results
were obtained by YAP and ECL (a common lisp) + a unify.lisp program. If
somebody is interested he may find the pure interfaces in the attached
emb.tar.gz.

Being a Pure novice, I'm sure the "unify.pure" can be improved by a more
advanced user.

Kurt

[Albert Graef]

On 10/30/2012 04:58 PM, kp wrote:
> After an "odyssey" of trying to embed some logic systems into Pure in
> order to use their unification capabilities I came to the conclusion
> that the best way is - at least for me - to use a "Pure" implementation
> of a rule based algorithm.

Ha! I like that. :)

Looking through the Reduce code (those .red files) I can only wonder how
they got all that stuff working. Ok, this Rlisp language is able to do
symbolic processing all right, but the syntax seems so awkward for this
kind of thing nowadays.

> The Prolog engines (if embedded) may be rather slow and the powerful
> systems like 'ciao or 'XSB have "mangled" libraries. The best results
> were obtained by YAP and ECL (a common lisp) + a unify.lisp program. If
> somebody is interested he may find the pure interfaces in the attached
> emb.tar.gz.

Hmm, if you could add a little README file explaining what this is all
about then we could maybe add it to the wiki somewhere? Or should we
just let it rot in the ml archive?

> Being a Pure novice, I'm sure the "unify.pure" can be improved by a more
> advanced user.

That code looks good to me. Makes for a nice example, in any case. Is it
ok if I commit this to pure/examples?

Albert

--
Dr. Albert Gr"af
Dept. of Music-Informatics, University of Mainz, Germany
Email: Dr.G...@t-online.de, a...@muwiinfa.geschichte.uni-mainz.de
WWW: http://www.musikinformatik.uni-mainz.de/ag

[kp]

Am 02.11.2012 23:55, schrieb Albert Graef:

> Hmm, if you could add a little README file explaining what this is all
> about then we could maybe add it to the wiki somewhere? Or should we
> just let it rot in the ml archive?

Let it rot :) I'm sure we recall it if necessary.

>
>> Being a Pure novice, I'm sure the "unify.pure" can be improved by a more
>> advanced user.
>
> That code looks good to me. Makes for a nice example, in any case. Is it
> ok if I commit this to pure/examples?

of course.

>
> Albert
>

Here is a (imo) simplified version. I was still thinking in Lisp terms
but eventually got rid of the "lists".

---
/* ..

A syntactic unification algorithm in Pure
=========================================

Rererences:
-----------
Baader/Synder
http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
2.2.3. A rule-based approach, p. 448 ff

Martelli-Montanari
www.nsl.com/misc/papers/martelli-montanari.pdf

Wikipedia
http://en.wikipedia.org/wiki/Unification_(computer_science)

*/


// Term reduction (alias Decomposition)
// (f t_1 ... t_n) == (f s_1 ... s_n) -> t_1 == s_1, ... ,t_n == s_n.
tred ((a@_ b) == (c@_ d)) = tred (a==c), quote(b==d) ;
tred (x==y) = quote(x==y) ;

// Symbol clash if not
// (f t_1 ... t_n) == (f s_1 ... s_n), n > 0.
clash ((f@_ s)==(g@_ t)) = clash (f==g) ;
clash (x==y) = x~==y ;

// Occur check
// x in (f t_1 ... t_n) ?
occurs x::var (f@_ s)
= true if x === s ;
= occurs x f || occurs x s ;
occurs x f = f===x ;

// Unification
unify ((x==y) : xs) S = unify xs S if (x===y) ;
unify ((x::appl == y::var) : xs) S = unify ((y==x):xs) S ;
unify ((x::var == y) : xs) S
= false if occurs x y ;
= unify (reduce_with [x=>y] xs) ((reduce_with [x=>y] S)+[x=>y]) ;
unify ((x::appl == y::appl) : xs) S
= false if clash (x==y) ;
= unify ((list (tred (x==y)))+xs) S ;
unify [] X = X ;

//
// Usage: unify P S
// where P = [lhs1 == rhs1, ..., lhs_n == rhs_n] is a list of equations
// {to avoid eval use quote(lhs == rhs)}, and S is a list of substitutions
// of the form [s_1 => t_1, ... , s_n => t_n] as it is used in
// reduce_with [a=>b] expr.
//
// Note that 'reduce_with S P' may be used to check if S is correct.
//


// Examples:

let P1 = [f (g x) x == f y a];
let P2 = [f x (h x) y == f (g z) u z] ;
let P3 = [p a x (f y) == p u v w, p a x (f y)== p a s (f c),
p u v w == p a s (f c) ] ;

let P4 = [f x b (g z) == f (f y) y (g u)] ;
let P5 = [p a x (h (g z)) == p z (h y) (h y)] ;
let P6 = [p (f a) (g x) == p y y] ; // should fail => 0
let P7 = [p x x == p y (f y)] ; // should fail => 0

let P8 = [sin (x+y) == sin (u^2+v^2)] ;

let P9 = [c+b==a+c,a+b==b+c] ;
let P10 = [c+b==a+c,a+b==b+c,a*b==c*d] ;

// Run:

#! > unify P1 [] ;
#! [y=>g a,x=>a]
#!
#! > reduce_with ans P1 ;
#! [f (g a) a==f (g a) a]
#!
#! > unify P2 [] ;
#! [x=>g z,u=>h (g z),y=>z]
#!
#! > reduce_with ans P2 ;
#! [f (g z) (h (g z)) z==f (g z) (h (g z)) z]
#!
#! > unify P3 [] ;
#! [a=>u,x=>s,w=>f c,v=>s,y=>c]
#!
#! > reduce_with ans P3 ;
#! [p u s (f c)==p u s (f c),p u s (f c)==p u s (f c),p u s (f c)==p u s
(f c)]
#!
#! > unify P4 [] ;
#! [x=>f y,b=>y,z=>u]
#!
#! > reduce_with ans P4 ;
#! [f (f y) y (g u)==f (f y) y (g u)]
#!
#! > unify P5 [] ;
#! [a=>z,x=>h (g z),y=>g z]
#!
#! > reduce_with ans P5 ;
#! [p z (h (g z)) (h (g z))==p z (h (g z)) (h (g z))]
#!
#! > unify P6 [] ;
#! 0
#!
#! > unify P7 [] ;
#! 0
#!
#! > unify P8 [] ;
#! [x=>u^2,y=>v^2]
#!
#! > reduce_with ans P8 ;
#! [sin (u^2+v^2)==sin (u^2+v^2)]
#!
#! > unify P9 [] ;
#! [c=>a,b=>a]
#!
#! > reduce_with ans P9 ;
#! [a+a==a+a,a+a==a+a]
#!
#! > unify P10 [] ;
#! [c=>d,b=>d,a=>d]
#!
#! > reduce_with ans P10 ;
#! [d+d==d+d,d+d==d+d,d*d==d*d]
#!
#! >

[Albert Graef]

On 11/04/2012 09:14 PM, kp wrote:
>> That code looks good to me. Makes for a nice example, in any case. Is it
>> > ok if I commit this to pure/examples?
> of course.

Committed in rev. d45731fea367, thanks!

[kp]

Am 11.11.2012 21:51, schrieb Albert Graef:
> On 11/04/2012 09:14 PM, kp wrote:
>>> That code looks good to me. Makes for a nice example, in any case. Is it
>>>> ok if I commit this to pure/examples?
>> of course.
>
> Committed in rev. d45731fea367, thanks!
>

I suppose the recent one (4.11) looks nicer and is even shorter, isn't
it :)
The use of 'prefix conversion' seemed to me a bit 'lispy :)
Kurt

[Albert Graef]

On 11/14/2012 01:46 AM, kp wrote:
> I suppose the recent one (4.11) looks nicer and is even shorter, isn't
> it :)

Oops, I accidentally committed the old version. It's fixed now.