[PRL] Newton's Laws of Computation?

[Mitchell Wand]

Several things:

1.  Matthias, I knew you were going complain about beta vs. beta-value.  I
don't really want to get into the details of the formulations of these--
those are lower-order bits.  (I even thought about saying that in the
original message). The point is that these laws epitomize basic principles:

-- Church's Law captures the essence of functional computation
-- von Neumann's Law captures the essence of imperative computation
-- Hoare's Law captures the essence of reasoning via invariants
-- Peano's Law is the moral equivalent of invariant reasoning for functional
computation.

2.  re Peano's Law:  I intended this as the intellectual basis for the
design recipe. I considered some fancier structural induction, but decided
that I wanted something that was more self-contained and involved fewer
arbitrary choices.  So I formulated it as Peano induction.  Everything else
is a corollary.

3.  What were Olin's comments?  I didn't see them.

4.  Matthias wrote:

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


Of course we need more layers on top of this. You wouldn't build a software
system using just these laws, any more than you would build a bridge
directly from Newton's Laws.  We need Jacobians and Lagrangians and all the
stuff that physicists use to bridge the gap between Newton's Laws and the
real world.

5.  The one amendment I did like was the comment that vonNeumann's Law
(which should perhaps be called McCarthy's Law, since I think he was one who
formulated it) should carry a note that the operation can be performed in
constant time.  Of course that's false in any kind of multilayered memory
system (consider cache vs. web!), so I'm not sure how to express that. Maybe
this is a clue to the next layer.

--Mitch








On 3/19/07, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
>
> 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
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed