RE: [Axiom-developer] A curious algebra failure

[Weiss, Juergen]

Hi,

The file patches.lisp in the scratchpad sources from 1990 contained the
following line:

(defun |pmatch| (s p) (|pmatchWithSl| s p '(ok))) ;assoc with atom at
eol

to override the definition in c-util.boot.

Seems that pmatchWithSl returns nil when a match
is not possible, empty assoc list != nil when no substitutions are
necessary
for a match and an assoc list with substitutions otherwise. 

For example
  v:= ASSOC(p,al) => s=rest v or al
returns 't if (p,s) is in al.

So this function can never typecheck in ansi common lisp. The
usage seems to come from a time when alists could contain
atomic properties and associations as well.

By the way, I think the line must read

  v:= ASSOC(p,al) => s=rest v and al
                              ====

this makes much more sense logically and should typecheck with 
the   pmatch(s,p) == pmatchWithSl(s,p,[nil])


Regards

Juergen Weiss

Juergen Weiss     | Universitaet Mainz, Zentrum fuer Datenverarbeitung,
address@hidden| 55099 Mainz, Tel: +49(6131)39-26361, FAX:
+49(6131)39-26407
 

> -----Original Message-----
> From: address@hidden 
> [mailto:address@hidden
>  On Behalf Of Gabriel Dos Reis
> Sent: Sunday, August 12, 2007 12:52 AM
> To: address@hidden
> Subject: [Axiom-developer] A curious algebra failure
> 
> 
> Hi,
> 
>   This issue pops up while looking at a type error in
> src/interp/c-util.boot. 
> 
>   1.  The type error
> 
>      Consider the function pmatch() from c-util.boot
> 
>          pmatch(s,p) == pmatchWithSl(s,p,"ok")
> 
>      That function is essentially called by the compiler to check
>      whether an expression e in mode m is coercible to mode m', as
>      can be seen from coerceable() defined in compile.boot
> 
>        coerceable(m,m',e) ==
>        m=m' => m
>        -- must find any free parameters in m
>        sl:= pmatch(m',m) => SUBLIS(sl,m')
>        coerce(["$fromCoerceable$",m,e],m') => m'
>        nil
> 
>       Basically, the expression e of mode m is coercible to mode m' if
>          (a) m and m' are identical -- the identity conversion;
>    
>          (b) m and m' can be unified by instantiating variables in m
>               -- instantiatiion conversion, the case handled 
> by pmatch;
> 
>          (c) or by attempting the actual conversion and see what
>               happens -- the "speculative" call to coerce();
>          
>          (d) and that is all.
>         
> 
> 
>        So far, so good.
> 
>        Now, let's look at the definition of pmatchWithSl() in 
> c-util.boot:
> 
>          pmatchWithSl(s,p,al) ==
>            s=$EmptyMode => nil
>            s=p => al
>            v:= ASSOC(p,al) => s=rest v or al
>            MEMQ(p,$PatternVariableList) => [[p,:s],:al]
>            null atom p and null atom s and_
>                    (al':= pmatchWithSl(first s,first p,al)) and
>              pmatchWithSl(rest s,rest p,al')
> 
>        Essentially, pmatchWithSl() computes a substitution that would
>        make the pattern p match the value s.  It uses a simply minded
>        unification algorithm, and is probably not efficient but that
>        is not of concern here.
> 
>        A simple type inference shows that the third argument to
>        pmatchWithSl() must be an association list.  Therefore, the 
>        current definition of pmatch() is ill-formed.
> 
> 
>    2.  The correct definition of pmatch
> 
>        Now that we have established that the existing definition of
>        pmatch is incorrect, what should a correct definition look
>        like?  Well, the whole thing pmatch() computes is a `minimal'
>        substitution that makes p match s.  So, it should start with
>        the identity substituation (or null substitution) and updates
>        it as it goes through the unification process.  So the correct
>        definition is:
> 
>          pmatch(s,p) == pmatchWithSl(s,p,[nil])
> 
>        where [nil] stands for the identity substitution.
> 
> 
>    3.  The problem in Algebra bootstrap
> 
>        After correction of pmatch(), I started a fresh build with
>        maximum safety turn on.  Everything proceeded well till
>        compilation of MONAD.spad where I see a failure with the
>        following message:
> 
> --------------------------------------------------------------
> ----------
>    initializing NRLIB MONAD- for Monad& 
>    compiling into NRLIB MONAD- 
>    importing RepeatedSquaring S
>    compiling exported ** : (S,PositiveInteger) -> S
> ****** comp fails at level 1 with expression: ******
> error in function ** 
> 
> (S)
> ****** level 1  ******
> $x:= S
> $m:= (Join (SetCategory) (CATEGORY domain (SIGNATURE * ($ $ $))))
> $f:=
> ((((|n| # #) (|x| # #) (* # # #) (** # # #) ...)))
>  
>    >> Apparent user error:
>    Cannot coerce S 
>       of mode (Monad) 
>       to mode (Join (SetCategory) (CATEGORY domain (SIGNATURE 
> * ($ $ $)))) 
> 
> 
> 
> 
>         Looking at the definition of MONAD, reproduced below, I see no
>         reason to expect that the call to expt(x,n) should work. What
>         am I missing?
> 
> 
> Thanks,
> 
> -- Gaby
> 
> )abbrev category MONAD Monad
> ++ Authors: J. Grabmeier, R. Wisbauer
> ++ Date Created: 01 March 1991
> ++ Date Last Updated: 11 June 1991
> ++ Basic Operations: *, **
> ++ Related Constructors: SemiGroup, Monoid, MonadWithUnit
> ++ Also See:
> ++ AMS Classifications:
> ++ Keywords: Monad,  binary operation
> ++ Reference:
> ++  N. Jacobson: Structure and Representations of Jordan Algebras
> ++  AMS, Providence, 1968
> ++ Description:
> ++  Monad is the class of all multiplicative monads, i.e. sets
> ++  with a binary operation.
> Monad(): Category == SetCategory with
>     --operations
>       "*": (%,%) -> %
>         ++ a*b is the product of \spad{a} and b in a set with
>         ++ a binary operation.
>       rightPower: (%,PositiveInteger) -> %
>         ++ rightPower(a,n) returns the \spad{n}-th right 
> power of \spad{a},
>         ++ i.e. \spad{rightPower(a,n) := rightPower(a,n-1) * a} and
>         ++ \spad{rightPower(a,1) := a}.
>       leftPower: (%,PositiveInteger) -> %
>         ++ leftPower(a,n) returns the \spad{n}-th left power 
> of \spad{a},
>         ++ i.e. \spad{leftPower(a,n) := a * leftPower(a,n-1)} and
>         ++ \spad{leftPower(a,1) := a}.
>       "**": (%,PositiveInteger) -> %
>         ++ a**n returns the \spad{n}-th power of \spad{a},
>         ++ defined by repeated squaring.
>     add
>       import RepeatedSquaring(%)
>       x:% ** n:PositiveInteger == expt(x,n)
>       rightPower(a,n) ==
> --        one? n => a
>         (n = 1) => a
>         res := a
>         for i in 1..(n-1) repeat res := res * a
>         res
>       leftPower(a,n) ==
> --        one? n => a
>         (n = 1) => a
>         res := a
>         for i in 1..(n-1) repeat res := a * res
>         res
> 
> 
> 
> -- Gaby
> 
> 
> _______________________________________________
> Axiom-developer mailing list
> address@hidden
> http://lists.nongnu.org/mailman/listinfo/axiom-developer
>