The equality test seems to have a bug. axiom p:Integer->Integer Type: Void axiom p(x)==x Type: Void axiom p
Type: FunctionCalled(p) axiom t:Boolean:=(p=p) axiom Compiling function p with type Integer -> Integer
Type: Boolean axiom )set mess bot on
Type: Boolean In fact, in 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 axiom )show Mapping 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, ... --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. Category: Axiom Compiler => Axiom Interpreter |