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
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
