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

[Tim Daly]

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.
> >     
>
> Tim,
>
> 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

 SORT == ITERATED CONDITIONAL SWAP

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:
http://daly.axiom-developer.org/CONCORDIA.html

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

Tim