[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] Embedding Axiom (Hickey and fold/unfold) Folding and g

From: Tim Daly
Subject: [Axiom-developer] Embedding Axiom (Hickey and fold/unfold) Folding and generalization
Date: Sat, 21 Nov 2009 12:15:37 -0500
User-agent: Thunderbird (Windows/20090302)

Martin Baker wrote:
On Friday 20 November 2009 23:17:25 Tim Daly wrote:
There is an excellent talk by Rich Hickey about modelling time, identity, values,
perception, state, memory, etc.


While I was watching this talk I was wondering about the difference between the mainstream computing issues verses mathematical computing issues.

I get the impression that the mainstream issue, from this talk, is about how to run multiple algorithms in parallel?

If we are trying to solve a set of equations, is there a natural parallelism ? For the reasons discussed in the talk, should a rule based method be preferred wherever possible and explicit coding of algorithms be discouraged?

Martin Baker

Folding and Unfolding via pattern matching....

On the second point, which is the subject of folding and unfolding I think that rules would be very useful here. Consider two statements (function calls) that you would like to prove are equal. The suggestion is to unfold them both by doing substitution of definitions until they are both "the same".... where "the same" means that they
exhibit the same pattern with substitution e.g.

 (x^2) == (y^2) where x->y

If two functions unfold to the same pattern then we can re-fold them into each other.

I think that this might be a key step in Axiom's development. I am trying to discover a way to prove Axiom programs correct. In particular, it would be good to prove that the operations in the domain Group actually follow from the "group axioms".
Can mathematical group axioms be unfolded into domain Group operations? Can
ACL2 be used to prove that each unfolding step is correct? (insert PhD students here).

The really clever trick is to do folding without knowing anything. This would be a form of "generalization". You are trying to find a way to recognize that a particular sequence of code "is a SORT routine", for instance. After all, if you can recognize
a "SWAP" sequence, a "CONDITIONAL" sequence, and an "ITERATION"
sequence, can you know that


This is a subject of a paper I'm going to present at HICSS in January.
An early video of the project ideas is at:

(The talk is in the context of function extraction and malware but the ideas are
motivated by my "prove computational math" struggles)

Generalization by folding would amount to finding the formula from an instance. The formula has much less information than the instances of the formula so all types
of generalization involve deliberately losing information.

It is not possible (well...caveats) to generalize from a single instance. The single instance can be generalized in many directions. Multiple instances give a way to generalize by comparing the instances to their fit in the generalized pattern.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]