Edit detail for #226 Equality in FunctionCalled revision 1 of 3

changed:
-
The equality test seems to have a bug.
\begin{axiom}
p:Integer->Integer
p(x)==x
p
t:Boolean:=(p=p)
)set mess bot on
t:=(p=p)
\end{axiom}


In fact, in 'variable.spad', the result should be true always.

\begin{verbatim}
)abbrev domain FUNCTION FunctionCalled
++ Description:
++ This domain implements named functions
FunctionCalled(f:Symbol): SetCategory with 
        name: % -> Symbol 
                ++ name(x) returns the symbol
  == add
   name r                 == f
   coerce(r:%):OutputForm == f::OutputForm
   x = y                  == true
   latex(x:%):String      == latex f
\end{verbatim}

So the code has no bugs! The Interpreter uses the wrong equality test function.
 Moreover, even this function gives the wrong answer. According to the ')set mess bot on message', the test function is taken from the domain '(INT->INT)', which is 'Mapping(INT, INT)'. Unfortunately, Mapping is an Axiom primitive and according to available documentation:

\begin{axiom}
)show Mapping
\end{axiom}

In any case, according to Hyperdoc, there is only one function exported: (you guessed it) equality testing. I have no idea where the code is or how the testing is done. Equivalence of functions (lambda terms) is undecidable, so I suppose equality here means equality in implementation? But surely, 'p' should be equal to 'p' however you test it.

Submitted by : (unknown) at: 2007-11-17T22:11:48-08:00 (16 years ago) Name : Axiom Version : default friCAS-20090114 Axiom-20050901 OpenAxiom-20091012 OpenAxiom-20110220 OpenAxiom-Release-141 Category : general Severity : critical serious normal minor wishlist Status : open pending closed Optional subject :   Optional comment :

The equality test seems to have a bug.

axiom
p:Integer->Integer

Type: Void

axiom
p(x)==x

Type: Void

axiom
p

(1)

Type: FunctionCalled? p

axiom
t:Boolean:=(p=p)

axiom

Compiling function p with type Integer -> Integer

(2)

Type: Boolean

axiom
)set mess bot on
t:=(p=p)
 Function Selection for =
      Arguments: ((INT -> INT),(INT -> INT)) 
      Target type: BOOLEAN 
 [1]  signature:   ((INT -> INT),(INT -> INT)) -> BOOLEAN
      implemented: slot (Boolean)$$ from (INT -> INT)

(3)

Type: Boolean

In fact, in variable.spad, the result should be true always.

So the code has no bugs! The Interpreter uses the wrong equality test function. Moreover, even this function gives the wrong answer. According to the )set mess bot on message, the test function is taken from the domain (INT->INT), which is Mapping(INT, INT). Unfortunately, Mapping is an Axiom primitive and according to available documentation:

axiom
)show Mapping
   Mapping(T, S, ...)
      Mapping takes any number of arguments of the form:
         T, a domain of category SetCategory
         S, a domain of category SetCategory
         ...
      Mapping(T, S, ...) denotes the class of objects which are 
      mappings from a source domain (S, ...) into a target domain T.
      The Mapping constructor can take any number of arguments. All 
      but the first argument is regarded as part of a source tuple 
      for the mapping. For example, Mapping(T, A, B) denotes the 
      class of mappings from (A, B) into T.
      This constructor is a primitive in FriCAS. For more 
      information, use the HyperDoc Browser.

In any case, according to Hyperdoc, there is only one function exported: (you guessed it) equality testing. I have no idea where the code is or how the testing is done. Equivalence of functions (lambda terms) is undecidable, so I suppose equality here means equality in implementation? But surely, p should be equal to p however you test it.