[Axiom-developer] A curious algebra failure

[Gabriel Dos Reis]

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