"Maxwell's equations of software" examined (2008)

[hegzploit]

http://www.righto.com/2008/07/maxwells-equations-of-software-examined.html

[YeGoblynQueenne]

Pf. Too convoluted. You have to define stuff in M expressions and then map them to S expressions. And what is it that you're defining? A set of primitive functions, some of them operating on specialised data structures. Why? Here's Prolog in Prolog:

  prove(true).
  prove((L,Ls)):-
      prove(L)
     ,prove(Ls).
  prove(L):-
      clause(L,Body)
     ,prove(Body).

  clause(H:-B,B).
  clause((H:-),true).

This is just a straight-forward implementatio of SLDNF Resolution [1]. No "primitives", no data types, no specialised data structures and no translation from Prolog to something else before looping back to Prolog.

Also, rather fewer LOCs. LISP people are always bragging about their LOCs. I don't know why.

__________

[1] "SLDNF" Resolution is Selective Linear Definite Resolution with Negation as Failure, officially; or, Straight-up Logical Derivations with No Fuckups Resolution, as I prefer to think of it.

[YeGoblynQueenne → YeGoblynQueenne]

To be clear, this is how you write your clauses so that the meta-interpreter can read them, not how clause/2 is implemented in practice:

  clause(H:-B,B).
  clause((H:-),true).

Should've made that clear up front :0

[FullyFunctional]

I feel a little sick every time I see this regurgitated; McCarthy's interpreter is not remotely in the same class as Maxwell's equations (and the Church-Turing thesis). It's neither axiomatic, universal, nor minimal. Good ol' lambda calculus does a much better job. For example, here's the lambda calculus self-interpreter [1]

  (\f. (\x.f(xx)) (\x.f(xx)) (\em.m(\x.x)(\mn.em(en)) (\mv.e(mv)))

[1] https://crypto.stanford.edu/~blynn/lambda/

[JonChesterfield → FullyFunctional]

Could you expand on that? It's not minimal but it states axioms and defines an interpreter for itself on top of them which sounds universal.

Lambda is dubious as a 'minimal' primitive in lisp as it embeds an implicit call to eval and implies more of them at the call site

[bear8642 → FullyFunctional]

Could you explain how that expression works? Recognise the Y combinator on the left but don't understand the right sub-expression

[jart → bear8642]

It's a good question, if we consider that it's been unanswered on the computer science stack exchange for four years. https://cs.stackexchange.com/questions/83533/practical-usage...

Basically, it does beta normal form reduction. In these kinds of situations, I sometimes feel like it's just as valuable to know how to get the darn thing to run, and then the rest explains itself. So for the purposes of this explanation, I'll share a Hello World example for this interpreter, that should hopefully get you going. This won't cover beta reduction or any of that jazz. Just the simplest possible usage that you can type into the web page at https://crypto.stanford.edu/~blynn/lambda/ and see something happen.

    (\a.(\b.a(b b))(\b.a(b b)))(\a.\b.b(\c.c)(\c.\d.a c(a d))(\c.\d.a(c d)))(\a.\b.\c.c(\d.\e.\f.\g.e d))
    # a.k.a. Y(λab.b(λc.c)(λcd.ac(ad))(λcd.a(cd)))(λabc.c(λdefg.ed))
    # a.k.a. [[Y λλ [[[0 λ 0] λλ [[3 1] [3 0]]] λλ [3 [1 0]]]] λλλ [0 λλλλ [2 3]]]

It should spit out the identity function:

    λd.d

Why did this happen? It's because Y(λab.b(λc.c)(λcd.ac(ad))(λcd.a(cd))) is the reducer a.k.a. E and λabc.c(λdefg.ed) is the argument. What is λabc.c(λdefg.ed)? It's an encoded version of the identity function λd.d. So in other words, all it did was output exactly what was inputted. Except the input had to be encoded. Why is it encoded? Normally in LISP, if we wanted to pass a program to a self-interpreter, we've wrap the argument in (QUOTE), e.g.

    (EVAL (QUOTE (LAMBDA (X) X)))

However the lambda calculus doesn't have a QUOTE builtin. Because the lambda calculus is a programming language that has only has a single keyword (can you guess what it is?) What they had to do instead was design a system of quoting that only uses lambdas:

    Var=\m.\a b c.a m
    App=\m n.\a b c.b m n
    Lam=\f.\a b c.c f

Or if you prefer SectorLambda notation:

    var="λλλλ [2 3]"
    app="λλλλλ [[1 4] 3]"
    lam="λλλλ [0 3]"

So if you want to derive the argument yourself, you can type the following into the Stanford web page.

    Lam (\y.Var y)
    => λa b c.c(λy a b c.a y)

You can even use the self-interpreter with SectorLambda. https://justine.lol/lambda/ For instance, the behavior of the reduced output will be the same as if you just typed in the normal identity function:

    { printf %s 'Y(λab.b(λc.c)(λcd.ac(ad))(λcd.a(cd)))(λabc.c(λdefg.ed))' | lam2bin.com; printf '0101'; } | blc; echo
    0101
    { printf %s 'λa.a' | lam2bin.com; printf '0101'; } | blc; echo
    0101

Another fun exercise, if you want to see all the steps that take place in reducing the self-interpreter, would be to download the lambda.com and lam2bin.com programs, and run the following command:

    printf %s 'Y(λab.b(λc.c)(λcd.ac(ad))(λcd.a(cd)))(λabc.c(λdefg.ed))' | lam2bin.com | lambda.com -vl
    Y (λab.b (λc.c) (λcd.a c(a d)) (λcd.a(c d))) (λabc.c (λdefg.e d))
    λa.a ⍆ Y (λab.b (λc.c) (λcd.a c(a d)) (λcd.a(c d))) (λabc.c (λdefg.e d)) ⋯
    a ⍆
        a=(Y (λbc.c (λd.d) (λde.b d(b e)) (λde.b(d e))) (λbcd.d (λefgh.f e)) ⋯)
    Y λab.b (λc.c) (λcd.a c(a d)) (λcd.a(c d)) λabc.c (λdefg.e d) ⋯ ⍆
    λb.a(b b) λb.a(b b) λabc.c (λdefg.e d) ⋯ ⍆
        a=λbc.(c (λd.d) (λde.b d(b e)) (λde.b(d e)))
    a b b λabc.c (λdefg.e d) ⋯ ⍆
        b=λc.(b(c c))
        a=λbc.(c (λd.d) (λde.b d(b e)) (λde.b(d e)))
    λab.b (λc.c) (λcd.a c(a d)) (λcd.a(c d)) b b λabc.c (λdefg.e d) ⋯ ⍆
    λb.b (λc.c) (λcd.a c(a d)) (λcd.a(c d)) λabc.c (λdefg.e d) ⋯ ⍆
    ...

Hope this helps!

See also https://web.archive.org/web/20180714080803/http://repository...

[YeGoblynQueenne → jart]

Sorry, I know this will come across as a little rude but, a "fun exercise"? My eyes hurt! Can't you do all this in a simpler notation? This looks like someone sneezed over a Scrabble set.

Edit: I guess that's more than a little rude. I apologise in advance, but really, this is so hard to read and I reckon it must be very hard to write correctly, let alone check the correctness off. There must be a better way!

[dang]

Related:

“Maxwell's equations of software” examined (2008) - https://news.ycombinator.com/item?id=23321955 - May 2020 (47 comments)