“Maxwell's equations of software” examined (2008)
righto.com
righto.com
A meta circular interpreter working on a simple binary encoding of lambda calculus (where abstraction is 00, application is 01, and a variable is 1^{n}0) is only 206 bits long [1][2], over 20 times smaller than the article's equations.
https://en.m.wikipedia.org/wiki/Wolfram%27s_2-state_3-symbol...
[1] https://tromp.github.io/cl/Binary_lambda_calculus.html#Brain...
In the more abstract one, you can emulate arbitrary computation by preparing the system (in case of the 2 state 3 symbol TM, its tape) in an appropriate configuration, letting it run until some the configuration satisfies some condition, and then extracting the result from the final configuration.
In a more concrete one, you have a language of programs, and a universal program takes a program description as input, and interprets it. I give a slightly more formal definition of such a notion of universality, as applicable to Algorithmic Information Theory, in [1].
[1] https://tromp.github.io/cl/Binary_lambda_calculus.html#Unive...
Furthermore, the complexity of beta reduction means that there are a multiplicity of strategies for executing it which are external to the definition of lambda calculus. Not so simple.
Lambda calculus also has a bias for the flow of information from the leaves of a term up to its root while demands flow from the root to the leaves. This is basically how functions work but it produces an asymmetry between a term and its environment. Higher order terms allow information to flow in very complex ways but there are simple computational ideas that are hard to capture in lambda calculus without monstrously complicated recursion schemes or modifications to lambda calculus. Think of the symmetric possibilities of flow of information in a spreadsheet.
Asynchronous computation, concurrent processing, and sharing of work have been with us since the dawn of computers and have their own basic mechanisms and principles, but they are at odds with beta reduction and functional information flow.
Lambda calculus is amazing but there surely is a frontier beyond it. Human reasoning is frequently biased to think functionally, in terms of inputs and outputs where outputs are treated differently from inputs, but the world and computation are full of relations and processes, too.
pop rx -> sp--; rx := mem[sp]
push rx -> mem[sp] := rx; sp++
sub rx ry -> rx := rx - ry
jmp rx $I -> if rx is zero jump $I bytes from end of instruction.
One might also argue: call rx -> mem[sp] := IP; sp++; IP := rx
ret -> sp--; IP := mem[sp]
nand rx ry -> rx := rx nand ry
but those are just optimizationsIt is very much more impressive that you can make a whole computer out of nothing but NAND or NOR gates, but still the same sort of thing.
I think if you'd call something "Maxwell's equations of software", a similar property should hold, somehow ...
https://physicstravelguide.com/equations/yang_mills_equation...
Anyone here knows what that could be ?
edit : i think the lesson was showing curry's work on combinator logic..
This is not the usual von Neumann encoding (https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_def...), so I think you may have started one level too encoded. The usual encoding puts 0 equal to the empty set, and n + 1 equal to the union of n (a set with n elements) and {n} (a singleton with 1 element).
In other words, if I understand the meaning of 'Etc.', your encoding puts
0 = {Ø}, 1 = {0, Ø} = {{Ø}, Ø}, 2 = {1, Ø} = {{{Ø}, Ø}, Ø}, …,
whereas the usual encoding puts 0 = Ø, 1 = 0 ∪ {0} = {Ø}, 2 = 1 ∪ {1} = {Ø, {Ø}}, ….
One advantage of this latter encoding is that the set n has n elements, and that the set n is n-times nested, in the sense that longest chain of elements x ∈ y ∈ z ∈ … ∈ n has length n. It also generalises nicely to ordinals (a transfinite generalization of the natural numbers), as explained in the above link (https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_def...).Any idea what they were - as my final year project of my CS degree I did an implementation of a simple purely functional programming language that macro expanded into lambda calculus and then was converted into various sets of combinators for evaluation (from SK upwards). I thought there was actually a stunning lack of weirdness and inconsistency - mind you this did also come with a stunning lack of performance!
NB The trickiest bit of the whole project was writing a garbage collector so I could actually get these things to run on a shared Unix mini-computer....
Edit: Getting Y (and therefore recursion) working purely in terms of SK still amazes me.
that was 20 years ago, but it made a big impression on me, so i think my memories are correct :)
[1] https://en.wikipedia.org/wiki/Whitespace_(programming_langua...