news-relayFrom: pop@edlab.cs.umass.edu (Robin Popplestone) 
Author Message
 news-relayFrom: pop@edlab.cs.umass.edu (Robin Popplestone)

Here is a version of Abelson and Sussman's Scheme version of unification
Note that the copyright remains with A&S, since it's but a translation.

/*
let.p                      Robin Popplestone MAY 1996

The following macro definition provides a "let" statement.

let
    jane = 7,
    joy = 6
in
    jane+joy
endlet

which would seem reasonably natural to users of Scheme and ML,
controls the scope of the declared variables, and avoids the
perennial pitfall of "lvars" namely that you can easily write:

   lvars jane = 4; joy = 34;

when you mean

   lvars jane = 4, joy = 34;

(the kind of feature regarded as a virtue in C...).

/* (C) Copyright, University of Massachusetts, June 1994, All Rights Reserved
 *
 * This program carries no warranty.
 *

 *

This program may reproduced for  academic and experimental purposes,  provided
the above attribution is preserved and extended as appropriate.

Commercial rights are reserved.

*/

====================================================================
*/

;;; let.p                   Robin Popplestone, spring 1995

define lconstant check_no_semicolon();
    lvars l,L = proglist, d=0;
    repeat; hd(L) -> l;
        if member(l, vedopeners) then d+1->d
        endif;
        if l == ";" and d == 0  then
            mishap('";" encountered in let binding', [^proglist]);
        endif;
        if member(l,vedclosers) then d-1->d;
        endif;
        if l = "in" and d==0 then ";" -> hd(L); quitloop;
        endif;
/*
        if d==0                           ;;; e.g. let + = Add in ....
        and isword(l)
        then lvars n = identprops(l);
            if  isnumber(n) and n>0
            and hd(tl(L)) == "="
            then
                identprops(l) -> hd(L);
                l::tl(L) -> tl(L);
                tl(L) -> L;
            endif
        endif;
*/
        tl(L) -> L;

    endrepeat;
enddefine;

define macro let;
  check_no_semicolon();
  "lblock", "lvars"
enddefine;

define macro endlet;
  "endlblock"
enddefine;

"let"::vedopeners -> vedopeners;
"endlet"::vedclosers -> vedclosers;
"in"::vedbackers->vedbackers;

/*

define test(x);
    let y = 1+x, z=3
        in y+z
    endlet
enddefine;

test()=>
*/
define AnExample(p);
    unless p then mishap('Example failed',[])
    endunless;
enddefine;

define assoc_scm(x,l);
    if null(l) then false
    elseif front(hd(l)) = x then hd(l)
    else   assoc_scm(x,tl(l))
    endif
enddefine;

<h3>2.1  Distinguishing Variables from Constants</h3>

<p>
The range  of possible  constants can  include Scheme  symbols, so  we  have a
problem in  distinguishing  between a  symbol  acting  as a  constant  and  as
variable, just as  we did in  Scheme itself. In  the logic paradigm,  however,
rather than use quotation  to distinguish symbols acting  as constants, it  is
more common to use some  other convention. In the  Lisp community it has  been
common to use a prefixed question mark. In this implementation we will treat a
variable as a list <tt>[? v )</tt> where <tt>v</tt>
is (conventionally) a symbol.

<pre><code>
define var_?(e);
    ispair( e) and hd(e) = "?"
enddefine;

</code></pre>

<p>
This means that any Scheme atom is a <em>constant</em>
in our representation of logic:

<pre><code>
define constant_? =  atom;
enddefine;
</code></pre>

<p>
and we may use <tt>equal?</tt> to determine if two constants are the same:

<pre><code>
define =_constant_? =  nonop =;
enddefine;
</code></pre>

<a name = "unification">
<h2>3  Implementing the Unification Algorithm</h2>

<h3>3.1  Binding variables to values; making frames</h3>

<p> To unify two terms <tt>t1</tt> and <tt>t2</tt> we must  <em>determining
a mapping  f  from  variables to  constants  under  which</em>  <tt>f(t1) =
f(t2)</tt>. We will refer to our representation of such a mapping as a <em>
frame</em>. However let us take an  abstract approach, and suppose that  we
have the following operations:

<pre>
make_binding      Makes a "binding" that is a pair associating
                  a variable with a value.

binding_in_frame  Finds a binding for a given variable in a frame

binding_value     Extracts the value component of a binding.

extend            Adds a new variable-value binding to a frame.
</pre>

<p>
We may implement these operations using a-lists for frames as follows:

<pre><code>
define make_binding = conspair;
enddefine;

define binding_in_frame = assoc_scm;
enddefine;

define binding_value = back;
enddefine;

define extend(var, val, frame);
    make_binding(var, val) :: frame
enddefine;

</code></pre>

<h3>3.2  The function unify</h3>

<p> To unify two  terms <tt>p1</tt> and <tt>p2</tt>  we write the  function
<tt>unify</tt>. It  takes  3 arguments,  <tt>p1,  p2 frame</tt>.  Here  the
<tt>frame</tt> serves the same  role as a frame  in the environment in  our
Scheme interpreter _ it remembers what variables have been bound to and  so
avoids having to  perform excessive  substitution. However in  the case  of
unification there  are  extra possibilities  that  have to  be  taken  into
account

<ul>
<li>
    Unification may not be possible. For example if we cannot unify 2 with 3
    To deal with this possibility, we allow the frame to take the value
    <tt>false</tt>. This should be distinguished from the empty frame
    <tt>[)</tt> which binds no
    variables. For example we may unify 2 with 2, and the resulting frame is
    <tt>[)</tt>. Note that here we are depending on the use of Scheme
    being implemented to the IEEE standard in which the empty list and the
    false truth value are distinct.
<li>
    Variables may be bound to variables. Thus <tt>[? x)</tt>
    unifies with <tt>[? y)</tt> as
    specified in the frame which we can think of as
    <tt>( ([? x) . [? y))).</tt> but which will actually print as
    <tt>( ([? x) ? y)).</tt>
</ul>
<p>
So let  us  consider  the  unification function.  Essentially  there  are  the
following cases to consider

<ul>
<li>
[1] <tt>frame</tt>
may be <tt>false</tt>.
This case  can arise because the unification has  already
failed but the code has not yet checked that this had happened. Checking  here
simplifies case [5] below. (As well as it being good practice to check for all
types of values an argument can have)

<li> [2] <tt>p1</tt> may  be a variable.  This case turns  out to be  quite
complicated, since <tt>p1</tt> may actually be bound in the  <tt>frame</tt>
and so is not free to be rebound. For example if we try to unify <tt>(+  [?
x) [? x))</tt> with <tt>(+ 2 3)</tt> we will first
 unify the  variable <tt>[?  x)</tt> with  <tt>2</tt> obtaining  the  frame
<tt>(([? x) .  2))</tt>. Then  we will need  to unify  <tt>[? x)</tt>  with
<tt>3</tt>. At this point the unification must fail. So we "pass the  buck"
to an auxiliary function unify_var.

<li> [3] <tt>p2</tt> may be  a variable. Again we call  <tt>unify_var</tt>,
but with its  arguments reversed.  This means  that the  first argument  of
<tt>unify_var</tt> is always guaranteed to  be a variable, simplifying  its
implementation.

<li> [4] If  <tt>p1</tt> is  a constant,  then <tt>p2</tt>  must also  be a
constant, and it must be the <em>same</em> constant.

<li> [5] If <tt>p2</tt> is a constant then <tt>p1</tt> could not have  been
a constant, so unification fails.

<li> [6] Otherwise  both <tt>p1</tt>  and <tt>p2</tt> must  be lists  which
represent complex  terms  and  not variables.  So  we  call  <tt>unify</tt>
recursively on the <tt>hd</tt> and  <tt>cdr</tt> of both. However we  have
to treat <tt>frame</tt> as a kind of  accumulator, in much the same way  as
we needed an  accumulator when  we were  making a  list of  the nodes  of a
ordered tree. So we  call <tt>unify</tt> on the  <tt>hd</tt>'s of the  two
terms [6.2]  obtaining a  new frame  which embodies  any variable  bindings
necessary to  unify the  <tt>cdr</tt>'s, and  then we  pass this  frame  to
another  call  of  <tt>unify</tt>  [6.1]   which  proceeds  to  unify   the
<tt>cdr</tt>'s, keeping the unification  consistent with the bindings  made
in the <tt>hd</tt>'s. </ul>

<pre><code>
define unify(p1, p2, frame);
    if     not(frame) then false                           ;;;[1]

    elseif var_?(p1)     then unify_var(p1, p2, frame)     ;;;[2]

    elseif var_?(p2)     then unify_var(p2, p1, frame)     ;;;[3]

    elseif constant_?(p1) then                             ;;;[4]
        if constant_?(p2) then
            if =_constant_?(p1, p2) then frame
            else false
            endif
        else false
        endif

    elseif constant_?(p2) then false                       ;;;[5]
    else                                                   ;;;[6]
        unify (
            tl(p1),                                        ;;;[6.1]
            tl(p2),
            unify(                                         ;;;[6.2]
                hd(p1),
                hd(p2),
                frame))
    endif
enddefine;
</code></pre>

<h3>3.3  The unify_var function unifies a variable with a term</h3>

<p> Now
we  come  to  the definition  of  <tt>unify_var</tt>.  There  is a
subtlety here that needs to be dealt with. What happens if we try to  unify
a variable with a term that <em>already contains the variable</em>. Suppose
we want  to  unify  a variable  <tt>[?  x)</tt>  with the  term  <tt>(f  [?
x))</tt>; we can  only do this  if we systematically  replace the  variable
<tt>[? x)</tt> with <tt>(f [?  x))</tt> everywhere in our terms,  including
<em>inside</em> the term <tt>(f [? x))</tt>. But this involves an  infinite
amount of work generating an infinite  term. This kind of thing can  happen
if we try to unify:

<pre>
    [g [? x] [f [? x]]]
    [g [? y] [? y]]
</pre>

<p> Standard logic does not allow  such a circular substitution to  happen,
and so  we have  to put  an <em>occurs  check</em> into  <tt>unify_var</tt>
which makes sure that we  do not unify a variable  with a term in which  it
occurs. [It should be ...

read more »



Sat, 20 Apr 2002 03:00:00 GMT  
 news-relayFrom: pop@edlab.cs.umass.edu (Robin Popplestone)

Here is a version of Abelson and Sussman's Scheme version of unification
Note that the copyright remains with A and S, since it's but a translation.

/* let.p Robin Popplestone MAY 1996 The following macro definition
provides a "let" statement.

let
    jane = 7,
    joy = 6
in
    jane+joy
endlet

which would seem reasonably natural to users of Scheme and ML, controls
the scope of the declared variables, and avoids the perennial pitfall
of "lvars" namely that you can easily write:

   lvars jane = 4; joy = 34;

when you mean

   lvars jane = 4, joy = 34;

(the kind of feature regarded as a virtue in C...).

/* (C) Copyright, University of Massachusetts, June 1994, All Rights Reserved
 *
 * This program carries no warranty.
 *

 *

This program may reproduced for  academic and experimental purposes,  provided
the above attribution is preserved and extended as appropriate.

Commercial rights are reserved.

*/

====================================================================
*/

;;; let.p                   Robin Popplestone, spring 1995

define lconstant check_no_semicolon();
    lvars l,L = proglist, d=0;
    repeat; hd(L) -> l;
        if member(l, vedopeners) then d+1->d
        endif;
        if l == ";" and d == 0  then
            mishap('";" encountered in let binding', [^proglist]);
        endif;
        if member(l,vedclosers) then d-1->d;
        endif;
        if l = "in" and d==0 then ";" -> hd(L); quitloop;
        endif;

        tl(L) -> L;

    endrepeat;
enddefine;

define macro let;
  check_no_semicolon();
  "lblock", "lvars"
enddefine;

define macro endlet;
  "endlblock"
enddefine;

"let"::vedopeners -> vedopeners;
"endlet"::vedclosers -> vedclosers;
"in"::vedbackers->vedbackers;

define AnExample(p); unless p then mishap('Example failed',[]) endunless;
enddefine; define assoc_scm(x,l); if null(l) then false elseif front(hd(l))
= x then hd(l) else assoc_scm(x,tl(l)) endif enddefine;

2.1 Distinguishing Variables from Constants
  -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -  

The range of possible constants can include Scheme symbols, so we have
a problem in distinguishing between a symbol acting as a constant and
as variable, just as we did in Scheme itself. In the logic paradigm,
however, rather than use quotation to distinguish symbols acting as
constants, it is more common to use some other convention. In the Lisp
community it has been common to use a prefixed question mark. In this
implementation we will treat a variable as a list    [? v )    where    v    is
(conventionally) a symbol.

   define var_?(e);
       ispair( e) and hd(e) = "?"
   enddefine;

This means that any Scheme atom is a ________        constant in our representation
of logic:

   define constant_? =  atom;
   enddefine;

and we may use    equal?    to determine if two constants are the same:

   define =_constant_? =  nonop =;
   enddefine;

3 Implementing the Unification Algorithm
  -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -  

3.1 Binding variables to values; making frames
  -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -  

To unify two terms    t1    and    t2    we must ___________           determining_  _ a_  _______       mapping_  _ f_  ____    from_  _________         variables
__  to_  _________         constants_  _____     under_  _____     which    f(t1) = f(t2)   . We will refer to our representation
of such a mapping as a _____     frame. However let us take an abstract approach,
and suppose that we have the following operations:

make_binding      Makes a "binding" that is a pair associating
                  a variable with a value.

binding_in_frame  Finds a binding for a given variable in a frame

binding_value     Extracts the value component of a binding.

extend            Adds a new variable-value binding to a frame.

We may implement these operations using a-lists for frames as follows:

   define make_binding = conspair;
   enddefine;

   define binding_in_frame = assoc_scm;
   enddefine;

   define binding_value = back;
   enddefine;

   define extend(var, val, frame);
       make_binding(var, val) :: frame
   enddefine;

3.2 The function unify
  -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -  

To unify two terms    p1    and    p2    we write the function    unify   . It takes
3 arguments,    p1, p2 frame   . Here the    frame    serves the same role as a
frame in the environment in our Scheme interpreter _ it remembers what
variables have been bound to and so avoids having to perform excessive
substitution. However in the case of unification there are extra possibilities
that have to be taken into account

     # Unification may not be possible. For example if we cannot unify
    2 with 3 To deal with this possibility, we allow the frame to take
    the value    false   . This should be distinguished from the empty frame
       [)    which binds no variables. For example we may unify 2 with 2,
    and the resulting frame is    [)   . Note that here we are depending
    on the use of Scheme being implemented to the IEEE standard in
    which the empty list and the false truth value are distinct.
     # Variables may be bound to variables. Thus    [? x)    unifies with    [?
       y)    as specified in the frame which we can think of as    ( ([? x)
       . [? y))).    but which will actually print as    ( ([? x) ? y)).

So let us consider the unification function. Essentially there are
the following cases to consider

     # [1]    frame    may be    false   . This case can arise because the unification
    has already failed but the code has not yet checked that this had
    happened. Checking here simplifies case [5] below. (As well as
    it being good practice to check for all types of values an argument
    can have)
     # [2]    p1    may be a variable. This case turns out to be quite complicated,
    since    p1    may actually be bound in the    frame    and so is not free
    to be rebound. For example if we try to unify    (+ [? x) [? x))    with
       (+ 2 3)    we will first unify the variable    [? x)    with    2    obtaining
    the frame    (([? x) . 2))   . Then we will need to unify    [? x)    with
       3   . At this point the unification must fail. So we "pass the buck"
    to an auxiliary function unify_var.
     # [3]    p2    may be a variable. Again we call    unify_var   , but with its
    arguments reversed. This means that the first argument of    unify_var
    is always guaranteed to be a variable, simplifying its implementation.

     # [4] If    p1    is a constant, then    p2    must also be a constant, and it
    must be the ____    same constant.
     # [5] If    p2    is a constant then    p1    could not have been a constant,
    so unification fails.
     # [6] Otherwise both    p1    and    p2    must be lists which represent complex
    terms and not variables. So we call    unify    recursively on the    hd
    and    cdr    of both. However we have to treat    frame    as a kind of accumulator,
    in much the same way as we needed an accumulator when we were making
    a list of the nodes of a ordered tree. So we call    unify    on the
       hd   's of the two terms [6.2] obtaining a new frame which embodies
    any variable bindings necessary to unify the    cdr   's, and then we
    pass this frame to another call of    unify    [6.1] which proceeds to
    unify the    cdr   's, keeping the unification consistent with the bindings
    made in the    hd   's.

   define unify(p1, p2, frame);
       if     not(frame) then false                           ;;;[1]

       elseif var_?(p1)     then unify_var(p1, p2, frame)     ;;;[2]

       elseif var_?(p2)     then unify_var(p2, p1, frame)     ;;;[3]

       elseif constant_?(p1) then                             ;;;[4]
           if constant_?(p2) then
               if =_constant_?(p1, p2) then frame
               else false
               endif
           else false
           endif

       elseif constant_?(p2) then false                       ;;;[5]
       else                                                   ;;;[6]
           unify (
               tl(p1),                                        ;;;[6.1]
               tl(p2),
               unify(                                         ;;;[6.2]
                   hd(p1),
                   hd(p2),
                   frame))
       endif
   enddefine;

3.3 The unify_var function unifies a variable with a term
  -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -   -  

Now we come to the definition of    unify_var   . There is a subtlety here
that needs to be dealt with. What happens if we try to unify a variable
with a term that _______       already_  ________        contains_  ___   the_  ________        variable. Suppose we want to
unify a variable    [? x)    with the term    (f [? x))   ; we can only do this
if we systematically replace the variable    [? x)    with    (f [? x))    everywhere
in our terms, including ______      inside the term    (f [? x))   . But this involves
an infinite amount of work generating an infinite term. This kind of
thing can happen if we try to unify:

    [g [? x] [f [? x]]]
    [g [? y] [? y]]

Standard logic does not allow such a circular substitution to happen,
and so we have to put an ______      occurs_  _____     check into  
...

read more »



Sat, 20 Apr 2002 03:00:00 GMT  
 
 [ 2 post ] 

 Relevant Pages 

1. news-relayFrom: pop@roo.cs.umass.edu (Robin Popplestone)

2. news-relayFrom: pop@roo.cs.umass.edu (Robin Popplestone)

3. news-relayFrom: pop@roo.cs.umass.edu (Robin Popplestone)

4. news-relayFrom: pop@roo.cs.umass.edu (Robin Popplestone)

5. news-relayFrom: pop@roo.cs.umass.edu (Robin Popplestone)

6. news-relayFrom: pop@edu.umass.cs.roo (Robin Popplestone)

7. news-relayFrom: pop@edu.umass.cs.roo (Robin Popplestone)

8. news-relayFrom: pop@edu.umass.cs.roo (Robin Popplestone)

9. news-relayFrom: pop@edu.umass.cs.winnie (Robin Popplestone)

10. news-relayFrom: pop@uucp.rabbit (pop)

11. news-relayFrom: jlc@uk.co.bmtech (jlc (Jonathan Cunningham))

12. news-relayFrom: kers@uk.co.hewlett-packard.hpl (Chris Dollin)

 

 
Powered by phpBB® Forum Software