[PRL] Newton's Laws of Computation?

[Mitchell Wand]

On 3/19/07, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
>
> On Mar 19, 2007, at 11:17 AM, Mitchell Wand wrote:
>
> > 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
>
> Hmph. Let's agree to disagree (for now), even on the bit value. [We
> can discuss off-line.]
>
> > -- von Neumann's Law captures the essence of imperative computation
> > -- Hoare's Law captures the essence of reasoning via invariants
>
> I'd rather see the use of projections/retracts. They are invariants
> and are as old as Hoare and I don't have to teach "ugly languages" to
> bring it across. To be precise, Floyd-Hoare comes with "baggage". It
> is the only law that people have recognized as fundamental, even in
> high school CS, without understanding its ramifications, the HUGE
> flaws [pointing back to FP] in Floyd-Hoar-Dijkstra-Gries approaches,
> etc.


I disagree.   State is fundamental.  It is what distinguishes computing from
mathematics, I am sorry to say.

And invariants are fundamental:  they express the essence of assume/require
reasoning.  In dealing with concurrent/distributed systems, that is the only
way to tame the complexity of real state.

Further, I claim that invarients are vital even in functional computing.  We
are always saying things like "this procedure assumes such-and-such a
relation between its arguments".   And we are always checking to make sure
that in each call to this procedure, the relation is guaranteed.  That's
just invariants in the functional setting.  (I have a great example of this,
but the margin is too small to contain it).

> -- Peano's Law is the moral equivalent of invariant reasoning for
> > functional computation.
>
> I am thinking of it more of a way to construct instances of invariants.
>
> > 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.
>
> Okay, I will agree to that.
>
> > 3.  What were Olin's comments?  I didn't see them.
>
> We had a private discussion on "Newton's laws" before I posed it to
> you. His (oral) reaction was "laws of algorithmic analysis, for
> example, bigO." I was incredulous and proposed "semantic laws" in
> response.
>
> > 4.  Matthias wrote:
> >
> > I don't think we need more than that. ...
> >
> > 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.
>
> My answer was given from a purely pedagogical perspective, i.e., CS 1
> ("210"). As you can probably imagine, you will have a really hard
> time teaching just a few of the ones you mentioned.
>
> From a general point of view, I naturally agree, but I am also
> afraid that as long as we stick to predictive laws, we will overlook
> the "constructive rules", which are of equal or even higher
> importance to engineers than Newton's laws.


I'm not clear on the distinction between "constructive" and "predictive".
For me, a constructive law is just one that predicts the behavior of the
artifact that is constructed using it.


> 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.
>
>
> Yes, I think that formulating laws in the spirit of "mathematical
> programs" (i.e., max this function, subject to these constraints) is
> precisely what we need. This is what I got out of my conversation
> with Olin.


Yes, I like this, too.

-- Matthias
>
>
> P.S. I think we should keep pushing this idea, write up a a paper on
> "Newton's Laws for Computer Science" and teach it in the Honors
> seminar or something like that to test its effectiveness.


Hmm, interesting idea.

--Mitch
-------------- next part --------------
HTML attachment scrubbed and removed