[Aldor-l] [Axiom-developer] spad: language and compiler

[Page, Bill]

On Wednesday, August 30, 2006 1:29 PM Jacques Carette wrote:
> 
> Gabriel Dos Reis wrote:
> > With Type:Type, it is not clear to me that when a well-typed
> > expression does not diverge, its value is not "wrong".
> >   
> Every 6 months or so, I tell Stephen he should write up a 
> formalization of Aldor's type system, and prove the usual
> Progress and Preservation theorems for it. 
> 

When it comes to the application of Aldor as the Axiom library
compiler, I am afraid that demanding that Aldor satisfy these
usual requirements might amount to "throwing the baby out with
the bath water".

The concept of "Progress" is very similar to well-foundedness.
By direct analogy with the theory of non-well-founded sets we
can have non-well-founded types which violate Progress but still
satisfy Preservation.

There is a growing literature on this subject.

http://portal.acm.org/ft_gateway.cfm?id=351261&type=pdf

Recursive Subtyping Revealed
Functional Pearl
Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pierce

http://www.dcs.ed.ac.uk/home/mf/TYPES/coinduction.ps

A Coinduction Principle for Recursive Data Types
Based on Bisimulation, by Marcelo Fiore

etc.

But I supposed Gaby would claim that these are still more
"vague allusions to co-inductive formalism" ;) Oh well...

Regards,
Bill Page.