[Top][All Lists]

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

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

From: Tim Daly
Subject: [Axiom-developer] Embedding Axiom (Hickey and fold/unfold)
Date: Fri, 20 Nov 2009 18:17:25 -0500
User-agent: Thunderbird (Windows/20090302)

There is an excellent talk by Rich Hickey about modelling time, identity, values,
perception, state, memory, etc.

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.

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.


reply via email to

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