help links subscribe changes refresh edit

	IssueTracker
#225 Series examples improvement idea ←	↑	→ #227 <code>random()$Integer</code> is a strange function

#226 Equality in FunctionCalled

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

	1 2 3
Editor: gdr Time: 2008/03/31 00:14:14 GMT-7
Note:

added:

From gdr Mon Mar 31 00:14:14 -0700 2008
From: gdr
Date: Mon, 31 Mar 2008 00:14:14 -0700
Subject: 
Message-ID: <20080331001414-0700@axiom-wiki.newsynthesis.org>

Category: Axiom Compiler => Axiom Interpreter

The equality test seems to have a bug.

axiom

p:Integer->Integer

Type: Void

axiom

p(x)==x

Type: Void

axiom

$\label{eq1}p \ x \ = = \ x$

(1)

Type: FunctionCalled(p)

axiom

t:Boolean:=(p=p)

axiom

Compiling function p with type Integer -> Integer

$\label{eq2} \mbox{\rm false}$

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

$\label{eq3} \mbox{\rm false}$

(3)

Type: Boolean

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

)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

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.

... --gdr, Fri, 25 Jan 2008 15:28:42 -0800 reply

I fear there is a confusion between the value of `p', and its type. The type of `p' is Integer -> Integer as stated in this declaration. Consequently the mode selection takes equality from Mapping(Integer,Integer), which is to return false all the type -- even if they functions are structurally equal (unlike pointer to functions in C).

`FunctionCalled? p' is the type, synthetized by the interpreter, for the value of `p'. This is one of the very cases where the type of an identifier does not agree with the value it refers to in the environement.

I'm afraid the definition of FunctionCalled? shown above does not capture the reality of the computations going on -- and I agree it is misleading.

... --gdr, Mon, 31 Mar 2008 00:14:14 -0700 reply

Category: Axiom Compiler => Axiom Interpreter