Edit detail for #110 Domain Variable() and Symbol revision 1 of 3

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).


\begin{axiom}
)clear all
)set output tex off
)set output algebra on
)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{spad}
)abbrev package SVT1 SymbolVariableTest1
SymbolVariableTest1(): Spec == Imp where
  Spec ==  with 
    symVar1:() -> Boolean
  Imp == add
    symVar1()==
      y: Variable(y) := y
      x: Variable(y) := y
      t: Boolean := (x = y)
\end{spad}

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


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

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

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

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{spad}
)abbrev package SVT4 SymbolVariableTest4
SymbolVariableTest4(): Spec == Imp where
  Spec ==  with 
    symVar4:() -> Boolean
  Imp == add
    symVar4()==
      y: Symbol
      x: Variable(y):=y
      t:Boolean:= true
\end{spad}

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{spad}
)abbrev package SVT5 SymbolVariableTest5
SymbolVariableTest5(): Spec == Imp where
  Spec ==  with 
   symVar5:() -> Boolean
  Imp == add
    symVar5()==
      y: Symbol := y
      x: Variable(y):=y::Variable(y)
      t:Boolean:= true
\end{spad}

(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{spad}
)abbrev package SVT6 SymbolVariableTest6
SymbolVariableTest6(): Spec == Imp where
  Spec ==  with 
   symVar6:() -> Boolean
  Imp == add
    symVar6()==
      y: Variable(y)
      x: Variable(y):=y
      t:Boolean:= x = y
\end{spad}

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{spad}
)abbrev package SVT7 SymbolVariableTest7
SymbolVariableTest7(): Spec == Imp where
  Spec ==  with 
   symVar7:() -> Boolean
  Imp == add
    symVar7()==
      y: Variable(y)
      x: Variable(y):=y
      t:Boolean:= x = x
\end{spad}

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

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

Computing the next result, which produces the error below in Windows version,
is not displayed properly by MathAction because the system error causes Axiom
to return an error condition.
<pre>
  symVar8()
</pre>

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>

From WilliamSit Mon Feb 21 18:14:07 -0600 2005
From: William Sit
Date: Mon, 21 Feb 2005 18:14:07 -0600
Subject: [#110 Domain Variable() and Symbol] improvementsin formatting of
	MathAction output
Message-ID: <421A794D.E4963CC5@cunyvm.cuny.edu>

Dear Bill:

Thanks for fixing some of the problems on MathAction in IssueTracker #110 and
also rebroadcasting the page.

Did you change the editor? The page is now defaulted to HTML+LaTeX and the
editor that came up when I hit the edit button is a fancy editor with tool bars.
On the other hand, I did not get the "raw" text. When I simply insert a carriage
return before the header "Compiler", the preview shows error. 

Resetting the format to Structured Text + LaTeX will mess up (line breaks, etc)
the preview as well.


William


From billpage Mon Feb 21 19:40:59 -0600 2005
From: billpage
Date: Mon, 21 Feb 2005 19:40:59 -0600
Subject: change of editor
Message-ID: <20050221194059-0600@page.axiom-developer.org>

William, I am sorry for this oversight. I did not intentionally
change the editor. I forgot that by default the wiki uses a "fancy
editor" called Epoz for the HTML page type. This editor assumes
that the content is pure HTML and is supposed to let people who
don't know HTML produce nicely formatted pages. Unfortunately the
pages that we are editing contain embedded LaTeX commands that
seem to completely confuse it. There is a way to change the mode to
plain text editing, but I think that on the whole this is more
trouble than it is worth. Therefore I have disabled Epoz and you
should be able to edit the HTML+LaTeX page in the same way as the
StructuredText+LaTeX pages.

The reason that I changed the page type to HTML+LaTeX is because I
have found that it often produces a better formated page when the
page contains compiler output.
---------
Bill Page.