[PRL] Newton's Laws of Computation?

[Matthias Felleisen]

Several responses rolled into one, now that I am off the 'net and  
have time :-]

1. I think you (Mitch) misunderstood my proposal to use retracts/ 
projections instead of Floyd-Hoare triples. A projection/retract is  
(imo) just the functional equivalent of an invariant, an overused  
word in CS. Just because you say "invariant" you don't have to use  
while-do loops. I think the word assertion is more descriptive of the  
Floyd-Hoare style than invariant in any case.

2. I also think you misunderstood my objection. It is entirely of  
historical-pedagogic nature. People will latch on to this and from  
there to imperative programming -- which is what we saw when high  
school model curricula in the 90s recommended logic. [Only advanced  
high schools covered anything but it was AP's reaction to the  
accusation that it was language-specific. The other reaction was big-O.]

3. Finally, I buy your argument that Flody-Hoare is imperative  
(pardon the pun) if you want to think about conventional thread-based  
programming. (Of course I should call this OWickie-Gries.) So yes, we  
need to include it in the list. -- And we should consider Erlang  
threads.

4. When I use the word "constructive" I don't mean laws that help me  
predict how my artifacts behave after I am finished constructing  
them. To me a "constructive rule/law" is something that helps me go  
from an empty sheet of paper and a problem statement to a solution on  
this empty sheet. The descriptive laws don't do anything like that.  
For this, engineers have "rule books" at least as far as EE and ChemE  
are concerned.

4a. I am still worried that coming up with just "predictive" laws  
will leave engineers rather unhappy. They will ask how to go from  
here to artifacts and then the majority will fall back on { ; } @ ->  
and similar things. We must show that "constructive rule books" exist  
in our world, and Design Patterns isn't enough (though I will admit  
that they have a leg up on us).

5. I want to propose another law along the lines of beta(v) and  
friends, but it is not at the same level:

                x : A
                f : A => B
  modus ponens ------------
                f(x) :   B


6. I like Joe's suggestion but I will frankly admit that I am not  
sure how to use it. Perhaps the program synthesis people are the  
answer to this quest for the Floyd-Hoare world and HtDP plus NUPRL  
are the pieces of the puzzle for the Gödel-Church world.

6a. Joe: I take "Newton's laws" as a metaphorical question here, not  
as a full-fledged distinction. But it's worth thinking about  
Hamiltonian and Lagrangian. Perhaps the way engineers use it suggests  
something for the constructive part.

7. Like Dan, I think sharing is more fundamental than assignment  
statement. Yes, for someone grown up in the imperative world, it  
looks like you need state change to get it, but at a higher-level  
(say DrScheme/Advanced) you just use shared. Or if you want to stay  
at the low level, just think of time passing by.

8. I thought a bit more about the connection to HtDP: In my mind, the  
discussion has confirmed why I chose the subtitle "an introduction to  
programming and computing" with the first referring to the  
"constructive" part and the second part referring to the "predictive"  
laws. Intermezzo 1 covers first-order beta, the intermezzo for iv  
covers beta. BigO is introduced to discuss vector-ref lookup NOT  
vector-set!. The last intermezzzo introduces the semantics of :=  
(set!) in the spirit of my dissertation not Floyd-Hoare. So I am  
happy but I want more.

Thanks! -- Matthias

On Mar 19, 2007, at 1:51 PM, Mitchell Wand wrote:

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