There is an excellent talk by Rich Hickey about modelling time,
identity, values,
perception, state, memory, etc.
http://www.infoq.com/presentations/Are-We-There-Yet-Rich-Hickey
I think it adds quite a bit to the Embedded Axiom idea set. If we kept
immutable
intermediate states we could easily run a computation forward and backward.
We can combine that immutable idea with the fold/unfold idea from functional
programming. The idea is that you can do program proofs by expanding
a definition by unfolding and contracting a definition by folding.
http://www.cs.nott.ac.uk/~gmh/bib.html#semantics
The analog of this idea, at least as I perceive it, is the same as doing
operations on both sides of an equation. If we want to prove things
about a computation we could work backward from the result by
unfolding to some intermediate point, and forward from the input by
unfolding to the same intermediate point. If they match then there is
a fold/unfold path between them.
Tim
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
