[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-developer] A curious algebra failure
From: |
Gabriel Dos Reis |
Subject: |
[Axiom-developer] A curious algebra failure |
Date: |
11 Aug 2007 17:52:14 -0500 |
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] A curious algebra failure,
Gabriel Dos Reis <=
- Re: [Axiom-developer] A curious algebra failure, Stephen Wilson, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Stephen Wilson, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Stephen Wilson, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Stephen Wilson, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/11
- Re: [Axiom-developer] A curious algebra failure, Stephen Wilson, 2007/08/11