login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Interpreter

In IssueTracker #99, I made some incorrect comments on how the Interpreter treats coercion between elements of the two domains Variable(x:Symbol) 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 Variable(x:Symbol) 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).

fricas
(1) -> )clear all
All user variables and function definitions have been cleared.
fricas
)set output tex off
 
fricas
)set output algebra on
 
fricas
)set mess bot on
Your user access level is compiler and this set option is therefore not available. See the )set userlevel command for more information. t:Boolean:= x = y
(1) false
Type: Boolean

Note when an undeclared identifier x is used, the interpreter temporarily turns it into the only element of Variable(x:Symbol), see (1) where x and y are interpreted as of type Variable(), not Symbol. Unlike Symbol, there is no equality testing across different Variable() domains and so in (1) both x and y are coerced to Symbol.

fricas
x:Variable(y):= y
(2) y
Type: Variable(y)

This is confirmed by (2), where the assignment is immediate because y:Variable(y).

So, when we get Symbol, this is via two stage process. First, identifier entered by the user is turnend into Variable(). Usually. this is only temporary. Namely, "interpreter" coercion machinery can coerce Variable() to a Symbol.

Why this two stage process? FriCAS wants to offer symbolic computation, that is users may write symbolic expression containing mathematical variables. But programming also needs variables. From implementation point of view the two kinds of variables are quite different: mathematical variables are data of some type, programming language variables store data. But we do not want any special notation to distinguish them. Instead FriCAS uses coercion machinery to assign role to identifiers. Variable(y) really says that FriCAS up to now did not decide if this is programming language variable or a symbolic one. Of course, once Variable(y) is stored in a variable it is data. But before that, during internal processing, interpreter can treat it as a programming language variable or coerce to a symbol. A symbol is a data, typically mathematical variable, but can be used in more general way.

When we manually declare the identifier as y: Variable(y), than it has this type. You cannot reassign with y:=1 later without changing the declaration of its type.

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

fricas
t:= ((x::Symbol)=y)
(3) true
Type: Boolean
fricas
t:= (x = (y::Symbol))
(4) true
Type: Boolean
fricas
)set mess bot off
Your user access level is compiler and this set option is therefore not available. See the )set userlevel command for more information.

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

The difference between y:Variable(y) and y:Symbol for the interpreter is thus that an undefined identifier y first is treated as Variable(y), but may be coerced to Symbol. And sometimes it need to be explicitly coerced to Symbol.

Compiler

Now, the real confusion is when one starts using the compiler!

Also there is a problem with MathAction/Wiki processing a comment line such as

--%SymbolVariableTest1

So these are omitted from below.

(a) Without any prior declarations or assignments, you can compile within a routine, y: Variable(y):= y (SVT1 below) but not x: Variable(y):= y (SVT2). Both are acceptable in the interpreter. So in the first case, the y on the rhs is of type Variable(y), 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.

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)
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2836962772639158623-25px004.spad
      using old system compiler.
   SVT1 abbreviates package SymbolVariableTest1 
------------------------------------------------------------------------
   initializing NRLIB SVT1 for SymbolVariableTest1 
   compiling into NRLIB SVT1 
   compiling exported symVar1 : () -> Boolean
Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |SymbolVariableTest1| REDEFINED
;;; *** |SymbolVariableTest1| REDEFINED Time: 0 SEC.
Warnings: [1] symVar1: y has no value
Cumulative Statistics for Constructor SymbolVariableTest1 Time: 0 seconds
finalizing NRLIB SVT1 Processing SymbolVariableTest1 for Browser database: --->-->SymbolVariableTest1(constructor): Not documented!!!! --->-->SymbolVariableTest1((symVar1 ((Boolean)))): Not documented!!!! --->-->SymbolVariableTest1(): Missing Description ; compiling file "/var/aw/var/LatexWiki/SVT1.NRLIB/SVT1.lsp" (written 12 MAY 2025 12:39:56 PM):
; wrote /var/aw/var/LatexWiki/SVT1.NRLIB/SVT1.fasl ; compilation finished in 0:00:00.004 ------------------------------------------------------------------------ SymbolVariableTest1 is now explicitly exposed in frame initial SymbolVariableTest1 will be automatically loaded when needed from /var/aw/var/LatexWiki/SVT1.NRLIB/SVT1

fricas
symVar1()
(5) true
Type: Boolean

spad
)abbrev package SVT2 SymbolVariableTest2
SymbolVariableTest2(): Spec == Imp where
  Spec ==  with 
    symVar2:() -> Boolean
  Imp == add
    symVar2()==
      x: Variable(y):=y
      t:Boolean:= true
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2427935065936506711-25px006.spad
      using old system compiler.
   SVT2 abbreviates package SymbolVariableTest2 
------------------------------------------------------------------------
   initializing NRLIB SVT2 for SymbolVariableTest2 
   compiling into NRLIB SVT2 
   compiling exported symVar2 : () -> Boolean
****** comp fails at level 3 with expression: ******
error in function symVar2 
(SEQ (|:=| (|:| |x| (|Variable| | << y >> |)) | << y >> |) (|exit| 1 (|:=| (|:| |t| (|Boolean|)) |true|))) ****** level 3 ****** $x:= y $m:= (Variable y) $f:= ((((|x| #) (|symVar2| #) (|$DomainsInScope| # # #) (% # #) ...)))
>> Apparent user error: NoValueMode is an unknown mode

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

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
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8532403455899499600-25px007.spad
      using old system compiler.
   SVT3 abbreviates package SymbolVariableTest3 
------------------------------------------------------------------------
   initializing NRLIB SVT3 for SymbolVariableTest3 
   compiling into NRLIB SVT3 
   compiling exported symVar3 : () -> Boolean
Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |SymbolVariableTest3| REDEFINED
;;; *** |SymbolVariableTest3| REDEFINED Time: 0 SEC.
Warnings: [1] symVar3: y has no value
Cumulative Statistics for Constructor SymbolVariableTest3 Time: 0 seconds
finalizing NRLIB SVT3 Processing SymbolVariableTest3 for Browser database: --->-->SymbolVariableTest3(constructor): Not documented!!!! --->-->SymbolVariableTest3((symVar3 ((Boolean)))): Not documented!!!! --->-->SymbolVariableTest3(): Missing Description ; compiling file "/var/aw/var/LatexWiki/SVT3.NRLIB/SVT3.lsp" (written 12 MAY 2025 12:39:56 PM):
; wrote /var/aw/var/LatexWiki/SVT3.NRLIB/SVT3.fasl ; compilation finished in 0:00:00.004 ------------------------------------------------------------------------ SymbolVariableTest3 is now explicitly exposed in frame initial SymbolVariableTest3 will be automatically loaded when needed from /var/aw/var/LatexWiki/SVT3.NRLIB/SVT3

But running it gives an error:

fricas
symVar3()
>> System error: The variable |y| is unbound.

This error explains part of the difference: FriCAS types are parametrized and creation of actual type. that is substituting actual arguments into a type, happens at runtime. When code tries to substitute y into Variable(y) programming language variable y has no defined value, so substitution fails. Interpreter is more forgiving, converting identifier y into the corresonding symbol and passing that to Variable. Other differences have similar reason: interpreter is trying very hard to coerce data to expected type, while Spad compiler needs explicit coercions.

Also, note that compiler says '[1]? symVar3: y has no value' which warns us that y is uninitialized. But detection of uninitialized variables is not reliable, compiler may fail to see that variable is uninitialized, so this is only a warning, not an error.

Writing argument to Variable as "x"::Symbol ensures correct type in this place. But resulting type is beyond capability of Spad compiler, it does not see that y can give value of type 'Variable(y)':

spad
)abbrev package SVT3 SymbolVariableTest3a
SymbolVariableTest3a(): Spec == Imp where
  Spec ==  with 
    symVar3:() -> Boolean
  Imp == add
    symVar3()==
      x : Variable("y"::Symbol):=y
      t : Boolean:= true
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8433375712314001547-25px009.spad
      using old system compiler.
   SVT3 abbreviates package SymbolVariableTest3a 
------------------------------------------------------------------------
   initializing NRLIB SVT3 for SymbolVariableTest3a 
   compiling into NRLIB SVT3 
   compiling exported symVar3 : () -> Boolean
****** comp fails at level 3 with expression: ******
error in function symVar3 
(SEQ (|:=| (|:| |x| (|Variable| (|::| "y" (|Symbol|)))) | << y >> |) (|exit| 1 (|:=| (|:| |t| (|Boolean|)) |true|))) ****** level 3 ****** $x:= y $m:= (Variable (:: y (Symbol))) $f:= ((((|x| #) (|symVar3| #) (|$DomainsInScope| # # #) (% # #) ...)))
>> Apparent user error: NoValueMode is an unknown mode

The example y :Variable(y):=y is a special case. But we cannot x:Variable(y):=y if we declare y: Symbol (without assignment, SVT4).

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
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5583142712275742882-25px010.spad
      using old system compiler.
   SVT4 abbreviates package SymbolVariableTest4 
------------------------------------------------------------------------
   initializing NRLIB SVT4 for SymbolVariableTest4 
   compiling into NRLIB SVT4 
   compiling exported symVar4 : () -> Boolean
****** comp fails at level 2 with expression: ******
error in function symVar4 
(SEQ (|:| |y| (|Symbol|)) | << | (|:=| (|:| |x| (|Variable| |y|)) |y|) | >> | (|exit| 1 (|:=| (|:| |t| (|Boolean|)) |true|))) ****** level 2 ****** $x:= (:= (: x (Variable y)) y) $m:= NoValueMode $f:= ((((|y| #) (|symVar4| #) (|$DomainsInScope| # # #) (% # #) ...)))
>> Apparent user error: CANNOT ASSIGN: y OF MODE: (Symbol) TO: x OF MODE: (Variable y)

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 Union("failed", Variable(y)). So this differs from the interpreter.

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
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2956805564468662474-25px011.spad
      using old system compiler.
   SVT5 abbreviates package SymbolVariableTest5 
------------------------------------------------------------------------
   initializing NRLIB SVT5 for SymbolVariableTest5 
   compiling into NRLIB SVT5 
   compiling exported symVar5 : () -> Boolean
****** comp fails at level 3 with expression: ******
error in function symVar5 
(SEQ (|:=| (|:| |y| (|Symbol|)) |y|) (|:=| (|:| |x| (|Variable| |y|)) | << | (|::| |y| (|Variable| |y|)) | >> |) (|exit| 1 (|:=| (|:| |t| (|Boolean|)) |true|))) ****** level 3 ****** $x:= (:: y (Variable y)) $m:= $EmptyMode $f:= ((((|x| #) (|y| # #) (|symVar5| #) (|$DomainsInScope| # # #) ...)))
>> Apparent user error: Cannot coerce y of mode (Symbol) to mode (Variable y)

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

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
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/7214572082810698305-25px012.spad
      using old system compiler.
   SVT6 abbreviates package SymbolVariableTest6 
------------------------------------------------------------------------
   initializing NRLIB SVT6 for SymbolVariableTest6 
   compiling into NRLIB SVT6 
   compiling exported symVar6 : () -> Boolean
****** comp fails at level 1 with expression: ******
error in function symVar6 
(|y|) ****** level 1 ****** $x:= y $m:= (Symbol) $f:= ((((|t| #) (|x| # #) (|y| #) (|symVar6| #) ...)))
>> Apparent user error: Cannot coerce y of mode (Variable y) to mode (Symbol)

Not even testing x=x (SVT7). Note that the compiler was apparently trying to use equality from Symbol, not equality from Variable(y). This is a bit bizarre. The identfiers x and y even after declaration to be of type Variable(y) 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 Variable(y). 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.)

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
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4490168181249298181-25px013.spad
      using old system compiler.
   SVT7 abbreviates package SymbolVariableTest7 
------------------------------------------------------------------------
   initializing NRLIB SVT7 for SymbolVariableTest7 
   compiling into NRLIB SVT7 
   compiling exported symVar7 : () -> Boolean
****** comp fails at level 1 with expression: ******
error in function symVar7 
(|y|) ****** level 1 ****** $x:= y $m:= (Symbol) $f:= ((((|t| #) (|x| # #) (|y| #) (|symVar7| #) ...)))
>> Apparent user error: Cannot coerce y of mode (Variable y) to mode (Symbol)

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

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)
spad
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/6938772839598774218-25px014.spad
      using old system compiler.
   SVT8 abbreviates package SymbolVariableTest8 
------------------------------------------------------------------------
   initializing NRLIB SVT8 for SymbolVariableTest8 
   compiling into NRLIB SVT8 
   compiling exported symVar8 : () -> Boolean
Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |SymbolVariableTest8| REDEFINED
;;; *** |SymbolVariableTest8| REDEFINED Time: 0 SEC.
Warnings: [1] symVar8: y has no value
Cumulative Statistics for Constructor SymbolVariableTest8 Time: 0 seconds
finalizing NRLIB SVT8 Processing SymbolVariableTest8 for Browser database: --->-->SymbolVariableTest8(constructor): Not documented!!!! --->-->SymbolVariableTest8((symVar8 ((Boolean)))): Not documented!!!! --->-->SymbolVariableTest8(): Missing Description ; compiling file "/var/aw/var/LatexWiki/SVT8.NRLIB/SVT8.lsp" (written 12 MAY 2025 12:39:56 PM):
; wrote /var/aw/var/LatexWiki/SVT8.NRLIB/SVT8.fasl ; compilation finished in 0:00:00.004 ------------------------------------------------------------------------ SymbolVariableTest8 is now explicitly exposed in frame initial SymbolVariableTest8 will be automatically loaded when needed from /var/aw/var/LatexWiki/SVT8.NRLIB/SVT8

fricas
symVar8()
>> System error: The variable |y| is unbound.

Note: The exact results depend on Lisp version and compilation settings. In particular at low safety settings accesses to uninitialized variables may produce arbitrary results. For example program may run but produce nonsense result. Or it may crash without any hint what happened.

fricas
)show SYMBOL
Symbol is a domain constructor. Abbreviation for Symbol is SYMBOL This constructor is exposed in this frame. 28 Names for 38 Operations in this Domain. ------------------------------- Operations --------------------------------
?<? : (%, %) -> Boolean ?<=? : (%, %) -> Boolean ?=? : (%, %) -> Boolean ?>? : (%, %) -> Boolean ?>=? : (%, %) -> Boolean OMwrite : (%, Boolean) -> String OMwrite : % -> String coerce : % -> OutputForm coerce : String -> % convert : % -> InputForm convert : % -> Pattern(Float) convert : % -> Pattern(Integer) convert : % -> Symbol elt : (%, List(OutputForm)) -> % hash : % -> SingleInteger latex : % -> String max : (%, %) -> % min : (%, %) -> % name : % -> % new : % -> % new : () -> % resetNew : () -> Void sample : () -> % scripted? : % -> Boolean smaller? : (%, %) -> Boolean string : % -> String ?~=? : (%, %) -> Boolean OMwrite : (OpenMathDevice, %, Boolean) -> Void OMwrite : (OpenMathDevice, %) -> Void argscript : (%, List(OutputForm)) -> % hashUpdate! : (HashState, %) -> HashState patternMatch : (%, Pattern(Float), PatternMatchResult(Float,%)) -> PatternMatchResult(Float,%) patternMatch : (%, Pattern(Integer), PatternMatchResult(Integer,%)) -> PatternMatchResult(Integer,%) script : (%, List(List(OutputForm))) -> % script : (%, Record(sub: List(OutputForm),sup: List(OutputForm),presup: List(OutputForm),presub: List(OutputForm),args: List(OutputForm))) -> % scripts : % -> Record(sub: List(OutputForm),sup: List(OutputForm),presup: List(OutputForm),presub: List(OutputForm),args: List(OutputForm)) subscript : (%, List(OutputForm)) -> % superscript : (%, List(OutputForm)) -> %

For example

fricas
X := matrix [[script(x,[[i],[j]]) for i in [1,2] ] for j in [1,2] ]
+ 1 1+ |y y | | 1 2| (6) | | | 2 2| |y y | + 1 2+
Type: Matrix(Polynomial(Integer))




  Subject:   Be Bold !!
  ( 15 subscribers )  
Please rate this page: