RE: [Axiom-developer] indefinites

[Bill Page]

William,

Thank you for bearing with my scepticism of the notion of
Indefinite Integer as a type.

On Saturday, June 26, 2004 11:56 PM William Sit
address@hidden wrote:
> 
> Bill Page wrote:
> > On Thursday, June 24, 2004 2:49 PM you Tim wrote:
> > >
> > > The distinction between Integer and Indefinite Integer is quite 
> > > subtle.
> > ...
> However, there should be no disagreement that the two
> mathematically are equivalent (that is, both obey the same 
> rules operating on integers) but computationally different.
>

I think we need to define more clearly what you mean by
"mathematically equivalent" and "computationally different",
but I don't think that I can agree that they are mathematically
equivalent, or at least not logically equivalent. For example
2=4 is a proposition but x=4 where x is an Integer is a predicate.
In the predicate calculus x=4 is neither true nor false until
we supply a quantifier or an instance. Computationally, at the
root of this is the notion of a (typed) lambda calculus. See
for example

  http://www.lfcs.inf.ed.ac.uk/reports/98/ECS-LFCS-98-381/

Programming languages like Haskel and the ML family pretty
much seem to have worked this out in detail. Perhaps what
you are trying to do is to make Axiom more "functional" in
the sense of these languages?

I will comment on other points in your email a little later.

Regards,
Bill Page.
 
> Bill continues:
> 
> > In the Axiom book p. 24 the expression x:Integer is called
> > a "declaration" and says only that it restricts the values 
> > that can be assigned to the variable, certain not that it
> > is no longer a variable simply because we have declared a
> > type! That's why I found Axiom's  behaviour very surprising.
> > ...