

last edited 14 years ago by gdr 
1 2 3  
Editor:
Time: 2007/11/17 21:53:04 GMT8 

Note: 
changed:  This following shows that functions in Axiom have types and a domain for functions may be associated with an identifier. \begin{axiom} dom:=(INT>INT) f:dom f x == x1 \end{axiom} However, when the function is compiled, the returned type displayed may not agree with its declared type or even its apparent compiled type and depends on the input! \begin{axiom} f 3 f(3) \end{axiom} This has nothing to do with the declaration of <code>f</code>. \begin{axiom} f(x:INT):INT==x1 f(3) f(3) \end{axiom} Not even: \begin{axiom} f(x:INT):INT==(x1)::INT f(3) f(3) \end{axiom} Or even: \begin{axiom} g(x:INT):NNI == 2^(sign(x)*x)::NNI g 3 \end{axiom} The following deliberate "error" shows the Interpreter always assumes <code>3</code> is of type <code>PositiveInteger</code>. \begin{axiom} f 3 f 3 \end{axiom} Compare the type returned below for <code>g 1</code>, the retraction to <code>PositiveInteger</code> is not done. \begin{axiom} g(x:INT): FRAC INT == 1/x g 1 \end{axiom} The difference may perhaps be due to the fact that the data structure of <code>FRAC INT</code> is very different from <code>INT</code>, whereas the data structure of <code>INT</code> is identical to that of <code>PI</code>. So the explanation that the reason <code>1/1</code> is not retracted because <code>retract</code> is not always possible is not the full story.
This following shows that functions in Axiom have types and a domain for functions may be associated with an identifier.
begin{axiom} dom:=(INT>INT) f:dom f x == x1 end{axiom}
However, when the function is compiled, the returned type displayed may not agree with its declared type or even its apparent compiled type and depends on the input!
begin{axiom} f 3 f(3) end{axiom}
This has nothing to do with the declaration of <code>f</code>.
begin{axiom} f(x:INT):INT==x1 f(3) f(3) end{axiom}
Not even:
begin{axiom} f(x:INT):INT==(x1)::INT f(3) f(3) end{axiom} Or even:
begin{axiom} g(x:INT):NNI == 2^(sign(x)*x)::NNI g 3 end{axiom}
The following deliberate "error" shows the Interpreter always assumes <code>3</code> is of type <code>PositiveInteger?</code>.
begin{axiom} f 3 f 3 end{axiom}
Compare the type returned below for <code>g 1</code>, the retraction to <code>PositiveInteger?</code> is not done.
begin{axiom} g(x:INT): FRAC INT == 1/x g 1 end{axiom}
The difference may perhaps be due to the fact that the data structure of <code>FRAC INT</code> is very different from <code>INT</code>, whereas the data structure of <code>INT</code> is identical to that of <code>PI</code>. So the explanation that the reason <code>1/1</code> is not retracted because <code>retract</code> is not always possible is not the full story.