[PRL] Newton's Laws of Computation?

[Matthias Felleisen]

On Mar 19, 2007, at 10:07 AM, Daniel Friedman wrote:

> Those of you who have looked at this problem, have you physically
> looked at the laws or just abstracted from the principle that we need

Ella asked the question in the following context. She's a Software  
Engineering professor in an Aero/Astro department (UMich). When the  
faculty meetings discuss educational issues, her "physical  
colleagues" just point to Newton's laws and that's pretty much that.  
If you don't know your mechanics and physics, you won't built  
rockets, planes, and helicopters. She has no such things to point to  
and as a result, her proposal/suggestions are exposed to the usual  
"fashion" discussions, which we all know so well from CS departments.  
[In Engineering, Fortran or C++ is it.]

> s small number of succinct laws?  There was a paper by some Oxford  
> people (cacm, if you can believe it) that addressed the
> algebraic laws of computation.  It might be a good starting place.


I believe I know the paper. It's some 15 years old and came from the  
Hoare group. It was mostly a first-order version of the Felleisen- 
Friedman-Hieb approach to semantics, without reference to our work of  
course.

-- Matthias



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