On Mar 19, 2007, at 8:49 AM, Mitchell Wand wrote:
> Matthias asked me the following question a couple of weeks ago:
>
> What are the equivalent of Newton's Laws for computation?
The question is due to Ella Atkinson (UMich, Aero).
> This morning I was surprised to discover that I already knew them.
> Here they are:
>
> First Law of Computation (Church's Law):
>
> ((\x.M) N) = M[N/x]
>
> Second Law of Computation (von Neumann's Law)
>
> (s[l=v])(l') = {v if l=l'
> {s(l') if l !=l'
Yes, I have expressed the same sentiments to Olin. And I do teach the
two above in 211, so my answer to Ella that HtDP is as good a
starting point as I know :-) was okay.
I do quibble with Mitch's response a little bit. I really really
think that it must be
((\x.M) V) = [V/x] M for V in some set of canonical forms
(specified as you desire)
Furthermore, after thinking about Olin's comments and suggestions --
radically different from Mitch's and completely wrong :-) -- I have
come to the conclusion that the second law should be
(s[l=v])(l') = v if l = l' and s(l') otherwise
subject to O(1)
i.e., the operation of looking up a value in the table s' should be
feasible in constant time (where s' is the modification of s at l).
I also think we should come up with a similar constraint for beta-V.
My proposed candidate for the constraint formulation is Will's
treatise on tail-recursion.
> Third Law of Computation (Hoare's Law)
>
> if P*B{S}P, then P{while B do S}P&~B
ARGH.
> Variant Version of Hoare's Law (Peano's Law)
>
> if P(0) and (all k)(P(k) => P(k+1)), then (all k)P(k)
Yes!!! I didn't teach this in 211, only appealing to their intuition
from high school, until I discovered that induction isn't covered in
high school in this country. I still didn't teach it after that
because I didn't know how to weave it in. Once Dale had Dracula
going, it was obvious: How to Prove Program is the next step. So this
is why I am so interested in getting the HtDP/ACL2 version of the
ground.
Quibble: I do think we shouldn't be happy with the N-based induction
but should immediately move to structural induction on algebraic data
types.
> These laws all have the property that they are succinctly stated, they
> embody an important principle for predicting the behavior of
> computations, and in order to understand them, you have to import an
> important body of knowledge about computation.
>
> So my question for the morning is: Can you state other laws of
> computation that are equivalently fundamental and succinct?
I don't think we need more than that. This keeps students busy for an
entire semester of "Newton for Computation". What we do need,
however, is a way to BUILD on these laws. Engineers don't study these
laws for nothing. Take laws like those for circuits and resistors
(Ohm) and so on. People use them to ask questions like "if I want a a
box that provides a resistor of blah Ohm based on the following
inputs, how to make this?" and then they fiddle with capacitors and
wires and resistors and show that the result satisfies the constraints.
So what we really need are ways to show that basing programs on
algebraic data types in a systematic manner is equivalent to using
Newton's laws for the construction of devices.
-- Matthias
>
> --Mitch
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl