Re: [Axiom-developer] Re: fixing SPAD

[Waldek Hebisch]

Martin Rubey wrote:
> "combinations of predicates through usual logical operators." *are* allowed.
> Only, in the context of conditional exports, predicates are limited to "is" 
> and
> "has".
> 
> Aldor, in contrast, makes no (or maybe, not much) difference to other parts of
> the code here.
> 
> Thus, my question is, would it be easy, or at least, doable for you, to make
> SPAD behave like Aldor here, i.e. drop the restriction on the predicates
> allowed?
>

There is a fundamental difficulty: theory of integers is undecidable, so
if you just add integer predicates to a dependent type system in style
of Barendregt book "Lambda calculi with types" you are likely to get
undecidable typesystem.

So, to get practical compiler you need to compromise.  I see some
possibilities here:

1) Defer typechecking to runtime
2) Reject some programs that are allowed by Barendregt style typesystem
3) Change point of view: instead of talking about types talk about 
   predicates (properties) satisfied by values in your program.
   Claiming that property holds is a mathematical theorem, so it
   requires a proof.  And programmer should write the proof together
   with the program.

I belive that Aldor goes for 1) (probably combined with unsoundness
in type system).  

In can imagine reasonable version of 2).  It should check each constructor
separately, and replace each predicate by combination of boolean
variables.  For each combination of values of boolean variables
the compiler should check if given variant is type-safe.  If all
variants are type safe the compiler should accept the program,
otherwise fail it.  Note that for various reasons values of predicates
may be dependent and some combinations of values may be excluded.
IIUC Barendregt style typesystem may notice some dependencies,
so it effectively will skip some impossibel combinations.  If possible
combinations type-check fine, but an impossible one fails then
Barendregt will accept the program but our rule will reject it.

Checking all variants may be expensive (if checking single variant
is linear the whole thing is co-NP), but we can hope that hard
cases will rarely occur.  BTW: It seems that Spad is already
doing similar thing with conditionals.

 
> > For a given specific case, one might look for a workaround that simulates
> > type checking at runtime.
> 
> I doubt this.  Of course, using Waldek's idea we could say that 'Complex F' is
> only allowed if either F is not a field or x^2+1 is irreducible in F.  But I'm
> not sure if that's what we want.  And I doubt that you can achieve what I 
> first
> proposed in current SPAD, namely, make 'Complex F' export 'Field' only if 
> x^2+1
> is irreducible in F.
>

I think that runtime checking idea is to allow Complex F, but when one
uses it as a Field check at runtime if it is ineded a Field (and signal
error if not).  I suspect that Spad is doing this already, but only
with conditions which it allows.
 
> I guess, your answer (whether it would be "easy"), is "no"...
> 

Doing thins Aldor way should be moderatly hard, say like implementing
extend.  It requires some real work and will not happen overnight.

Doing Barenrdregt style typesystem with arbitrary predicates?  Well,
this is a research problem.


-- 
                              Waldek Hebisch
address@hidden