On Wed, Jul 9, 2008 at 6:56 PM, Bill Page <[EMAIL PROTECTED]> wrote:
> On Wed, Jul 9, 2008 at 6:32 PM, Gabriel Dos Reis wrote:
>> On Wed, Jul 9, 2008 at 3:31 PM, Bill Page wrote:
>>> ...
>>> If you expect to be able to write:
>>>
>>> x:Float
>>> x+1.0
>>>
>>> what is the possible type of the result?
>>
>> Symbolic Float -- as explained in the `computing with unknowns' paper.
>>
>
> Ah, I wish I could be at the meeting in Bristol to discuss this in
> detail. Maybe at ISSAC?
I'll be at ISSAC.
>
>>> What operation is represented
>>> by '+'?
>>
>> The `+' there is the modemap for the + that operates on Floats. Note that
>> x + 1.0 is not a Float, therefore, the code that implements the `+' operation
>> is not called, until x is actually substituted with a Float value.
>>
>> The value x + 1.0 -- which is of type Symbolc Float, is internally
>> a typed AST, with the node trhe modemap for `+', and leaves, the
>> Float value 1.0 and the symbol x.
>>
>>> What are the types of it's arguments?
>>
>> See above.
>>
>
> So this involves both a new mode for evaluating expressions in the
> Interpreter as well as a new domain constructor? Sounds like a lot of
> work!
Sound symbolic computation has no price -- it seems. And it is not clear to
me that there actually are alternatives that require less work.
>
> What is the role of the argument to the domain constructor?
The argument T to the domain constructor says that when all the
unknowns are replaced by by their actual values, the result,
when defined is of type T.
> When is it used?
In both the synthesis and type checking of expressions. For example
x: Float
eval(['x="foo"], sin x)
is ill-formed.
> What is the result of evaluating something like this?
>
> x:Integer
> y:Float
> x+y
Symbolic Float.
Why? because assume for a second that x and y actually had a value,
then the interpreter would select the modemap +: (Float,Float) -> Float
and convert x to Float. The abstract syntax tree for x + y constructs
exactly that computation, except that the leaves are x and y.
You might think that that is lot of work. However, the machinery is
already in the interpreter when one is in compilation mode. It is just
a matter of adapting it with the new rule.
>
>>>
>>> In the Axiom interpreter, not specifying any type for x is equivalent
>>> to declaring
>>>
>>> x:Variable(x)
>>
>> No, that is absolutely false. Not declaring `x' results in the
>> interpreter evaluating the *expression* `x' to a value of type
>> Variable x with internal representation the symbol x.
>>
>> The key is to distinguish declaration from the evaluation of an
>> identifier as an expression.
>>
>
> In what sense is it not "equivalent"?
What reasons make you believe that evaluating an undeclared identifier
is equilavent, e.g. has exactly the same effects, as declaring that identifier
to be of type Variable x?
>
>>
>> In the augmented OpenAxiom interpreter, not giving a
>> value to x in
>>
>> x:Float
>>
>> results in the evaluation of the *expression* `x' to evaluate to
>> a value of type Symbolic Float with internal representation
>> the symbol x.
>
> So where the interpreter used to say:
>
> x is declared as being in Float but has not been given a value.
>
> it now inserts a value of this type.
Yes, that is what is explained in the paper.
> Does it apply to all types?
Almost -- except function types, which is already weird in
all AXIOM systems.
> What
> happens if I write:
>
> x:Polynomial Integer
>
> without providing any value. Is 'x' evaluated as Symbolic Polynomial
> Integer? If not, how is that prevented?
the *expression* x evaluates to a Symbolic Polynomial Integer.
The type of of the *variable* x remains Polynomial Integer in the
evaluation environment.
>
> -----
>
> I know these questions might lead to a lot of technical details, so if
> you would prefer to delay further discussion until we next meet, or at
> a later time please feel free.
Well, I hope to be there -- and I hope you would have read the paper before
then :-)
>
> I think this is an exciting development for OpenAxiom users and could
> have a big impact on it's acceptance in the community. Thanks!
You are welcome. The basic idea is to try to spell out how to
compute with typed ASTs. That requires lot of care, but the machinery
is not unduly horendous. Just think about how the interpreter compile
expressions, and you'll see the start of the path :-)
Of course, this development makes even more important the work
done by Andreas Dolzmann and Thomas Sturm as I pointed out here
http://www.mail-archive.com/[EMAIL PROTECTED]/msg13175.html
>
> Regards,
> Bill Page.
>
-------------------------------------------------------------------------
Sponsored by: SourceForge.net Community Choice Awards: VOTE NOW!
Studies have shown that voting for your favorite open source project,
along with a healthy diet, reduces your potential for chronic lameness
and boredom. Vote Now at http://www.sourceforge.net/community/cca08
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
