[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
RE: [Axiom-developer] A curious algebra failure
From: |
Weiss, Juergen |
Subject: |
RE: [Axiom-developer] A curious algebra failure |
Date: |
Sun, 12 Aug 2007 12:11:42 +0200 |
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
>
- [Axiom-developer] Re: .spad, .input, .as and autocoercion, (continued)
- [Axiom-developer] Re: .spad, .input, .as and autocoercion, Gabriel Dos Reis, 2007/08/16
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/14
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), William Sit, 2007/08/12
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/12
- Re: [Axiom-developer] A curious algebra failure, Martin Rubey, 2007/08/12
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/12
- Re: [Axiom-developer] A curious algebra failure, Gabriel Dos Reis, 2007/08/11
RE: [Axiom-developer] A curious algebra failure,
Weiss, Juergen <=