axiom-developer
[Top][All Lists]

[Axiom-developer] [#110 Domain Variable() and Symbol] Problems with Math

 From: wyscc Subject: [Axiom-developer] [#110 Domain Variable() and Symbol] Problems with MathAction, Compiler Date: Mon, 21 Feb 2005 01:16:18 -0600

Changes
http://page.axiom-developer.org/zope/mathaction/110DomainVariableAndSymbol/diff
--

??changed:
-
<B>Interpreter</B><br><br>

In IssueTracker #99, I made some incorrect comments on how the Interpreter
treats coercion between elements of the two domains
<code>Variable(x:Symbol)</code> and 'Symbol'. This new page consists of
experiments to find out more, in regard to both the Interpreter and the
Compiler. Note that the domain constructor <code>Variable(x:Symbol)</code>
contains a unique element with output representation 'x' which may be coerced
to the symbol 'x'. The domain 'Symbol' consists of all symbols (I know this
does not say anything, but I won't dare to say it consists of all undeclared
identifiers or all variables).  The following should have <code>)set mess bot
on</code>, but MathAction does not process this well.

\begin{axiom}
)clear all
--)set mess bot on
t:Boolean:= x = y
\end{axiom}

Note when an undeclared identifier 'x' is used, the interpreter temporarily
turns it into the only element of <code>Variable(x:Symbol)</code>, see (1)
where 'x' and 'y' are interpreted as of type <code>Variable()</code>, not
'Symbol'. Unlike 'Symbol', there is no equality testing across different
<code>Variable()</code> domains and so in (1) both 'x' and 'y' are coerced to
'Symbol'.
\begin{axiom}
x:Variable(y):= y
\end{axiom}

This is confirmed by (2), where the assignment is immediate because
<code>y:Variable(y)</code>.  Thus from 'Symbol' to <code>Variable()</code>
seems to me automatic *in the interpreter* but temporarily. Temporarily,
because you can reassign the identifier to any other typed value. This is
different than manually declaring the identifier as <code>y:
Variable(y)</code>. You cannot reassign with <code>y:=1</code> later without
changing the declaration of its type.

However, I was not able to find any function that does this: <code>y
+->Variable(y)</code> and we know why: the target domain is dependent on the
input.

\begin{axiom}
t:= ((x::Symbol)=y)
t:= (x = (y::Symbol))
--)set mess bot off
\end{axiom}

The absence of this map's signature may be why in (3), the Interpreter did not
coerce <code>x:Symbol</code> to <code>x:Variable(y)</code>, but did the
opposite. Same for (4), it coerces <code>x:Variable(y)</code> to
<code>x:Symbol</code>.

The difference between  <code>y:Variable(y)</code> and <code>y:Symbol</code>
for the interpreter is thus that an undefined identifier 'y' behaves as
'Symbol' only transiently on its way to 'Variable(y)', and need to be
explicitly coerced back to 'Symbol'.

<B>Compiler</B><br><br>

Now, the real confusion is when one starts using the compiler! (By the way, in
Windows 0.1.4 version, all compiling of the test packages, a message appears:

'The syntax of the command is incorrect.'

This does not appear below. Also there is a problem with MathAction/Wiki
processing a comment line such as

<code>--%SymbolVariableTest1</code>

So these are omitted from below.)

(a) Without any prior declarations or assignments, you can compile within a
routine, <code>y: Variable(y):= y</code> ('SVT1' below) but not <code>x:
Variable(y):= y</code> ('SVT2'). Both are acceptable in the interpreter. So in
the first case, the 'y' on the rhs is of type <code>Variable(y)</code>, but not
in the second case ('SVT2'), where it is untyped and unassigned. According to
Section 6.16 of the Axiom book, I think both 'y' on the rhs is free (global)
the first time it is encountered in the subroutines.

\begin{axiom}
)abbrev package SVT1 SymbolVariableTest1
SymbolVariableTest1(): Spec == Imp where
Spec ==  with
symVar1:() -> Boolean
symVar1()==
y: Variable(y) := y
x: Variable(y) := y
t: Boolean := (x = y)
\end{axiom}

\begin{axiom}
symVar1()
\end{axiom}

\begin{axiom}
)abbrev package SVT2 SymbolVariableTest2
SymbolVariableTest2(): Spec == Imp where
Spec ==  with
symVar2:() -> Boolean
symVar2()==
x: Variable(y):=y
t:Boolean:= true
\end{axiom}

(b) We can compile <code>x:Variable(y):=y</code> if we first declare <code>y:
Variable(y)</code> (without assignment, SVT3).

\begin{axiom}
)abbrev package SVT3 SymbolVariableTest3
SymbolVariableTest3(): Spec == Imp where
Spec ==  with
symVar3:() -> Boolean
symVar3()==
y: Variable(y)
x: Variable(y):=y
t:Boolean:= true
\end{axiom}

Even though 'y' was never defined, the function <code>symVar3()</code> still
runs. Actually the local variable 'x' is assigned 'Nil'.

\begin{axiom}
symVar3()
\end{axiom}

But we cannot <code>x:Variable(y):=y</code> if we declare <code>y:
Symbol</code> (without assignment, 'SVT4').

\begin{axiom}
)abbrev package SVT4 SymbolVariableTest4
SymbolVariableTest4(): Spec == Imp where
Spec ==  with
symVar4:() -> Boolean
symVar4()==
y: Symbol
x: Variable(y):=y
t:Boolean:= true
\end{axiom}

Not even if we assign a value to 'y' and we specify a coercion afterwards
('SVT5'). This is because no such coercion function exists (even if the target
is <code>Union("failed", Variable(y))</code>. So this differs from the
interpreter.

\begin{axiom}
)abbrev package SVT5 SymbolVariableTest5
SymbolVariableTest5(): Spec == Imp where
Spec ==  with
symVar5:() -> Boolean
symVar5()==
y: Symbol := y
x: Variable(y):=y::Variable(y)
t:Boolean:= true
\end{axiom}

(c) Although we can compile <code>x:Variable(y):=y</code> after declaring
<code>y:Variable(y)</code> without assigning a value to 'y' ('SVT3') and in
fact run <code>symVar3()</code>, we cannot compile a line actually using 'x'
('SVT6').

\begin{axiom}
)abbrev package SVT6 SymbolVariableTest6
SymbolVariableTest6(): Spec == Imp where
Spec ==  with
symVar6:() -> Boolean
symVar6()==
y: Variable(y)
x: Variable(y):=y
t:Boolean:= x = y
\end{axiom}

Not even testing <code>x=x</code> ('SVT7'). Note that the compiler was
apparently trying to use equality from 'Symbol', not equality from
<code>Variable(y)</code>. This is a bit bizarre. The identfiers 'x' and 'y'
even after declaration to be of type  <code>Variable(y)</code> may still be of
type 'Symbol'. On the other hand, an inspection of the code generated for
'SVT3' shows the equality is in fact from <code>Variable(y)</code>. So, why
does the compiler try to convert 'y' to 'Symbol'? Why does 'SVT6' fail to
compile? (I would expect it to compile, but give a run-time error.)

\begin{axiom}
)abbrev package SVT7 SymbolVariableTest7
SymbolVariableTest7(): Spec == Imp where
Spec ==  with
symVar7:() -> Boolean
symVar7()==
y: Variable(y)
x: Variable(y):=y
t:Boolean:= x = x
\end{axiom}

(d) But if we stay with the domain 'Symbol', we can compile without a problem
even if 'y' is never assigned ('SVT8').

\begin{axiom}
)abbrev package SVT8 SymbolVariableTest8
SymbolVariableTest8(): Spec == Imp where
Spec ==  with
symVar8:() -> Boolean
symVar8()==
y:Symbol:= y
x:Symbol:= y
t:Boolean:= (x=y)
\end{axiom}

For some unknown reasons, replacing <code>y:Symbol:=y</code> by
<code>y:Symbol</code>, which still compiles, causes MathAction not to display
correctly. MathAction should display correctly up to the place of error, but it
doesn't. Also, the next result, which produces the error below in Windows
version, is not displayed.

\begin{axiom}
symVar8()
\end{axiom}

Like <code>Variable(y)</code>, in 'SVT8', 'y' is considered undefined, but
unlike 'SVT1', 'SVT8' produces a run time error. Which one is a bug?

<pre>
>> System error:
equal: x is a NULL pointer

protected-symbol-warn called with (NIL)
</pre>

--