[Axiom-developer] Re: [Aldor-l] [Axiom-math] Are Fraction and Complex domains.

[Christian Aistleitner]

Hello,

> I'm
> converned with the type system.
>
> The type system allows for checking that expectations of functions are
> met by their arguments.  That checking, and reasoning in general,
> requires that we can replace equals for equals. If I defined a
> function with a given type (the type is evaluated to some type value), an
> later defined a variable or value of the same type (but this time, it
> gets evaluated to another type value), how can I even call the
> function with that variable?  And if the system let me do it, how can
> I prove that the call and the result are sound?

I designed the some really bad case for functional type systems and  
implemented it assuming Aldor would be functional (function.as) and  
assuming it is not functional (not_functional.as).

I do not see any problems with reasoning in both examples. As I already  
explained in my previous mail:
You can use a functional type system to simulate a non functional one.
And you claim it is possible to reason in a functional type system (which  
I do not doubt).

So, using your method of reasoning and my method of expressing non  
functionality by a functional type system allows you to reason in a non  
functional type system.

You can reason in a system with List( Integer ) and List( Character )  
being different. So it should not be a problem to reason in a system with  
List( Integer, timestamp ) and List( Integer, different timestamp ).

> | Besides, I am looking for a language, where same formalisms are  
> treated in
> | the same way.
> | For example all functions should be treated equal.
>
> The troubel is terms and types are generally of the "kind".

Sorry, but I am not familiar with the word "term" in this context. You  
probably do not mean terms as used for polynomials and probably also not  
term as in "mathematical expression" or as used in formal grammars.

Since large parts of your mail deal with "term" I'd better postpone the  
rest of my answer until I understand what you mean by "term".

--
Kind regards,
Christian

functional.as
Description: Binary data

non_functional.as
Description: Binary data