The Lambda Calculus (2023)
plato.stanford.edu
plato.stanford.edu
> One can represent natural numbers in a simple way, as follows:
> Definition (ordered tuples, natural numbers) The ordered tuple ⟨a0 , … an⟩ of λ-terms is defined as λx [x a0 … an]. One then defines the λ -term ┌ n ┐ corresponding to the natural number n as: ┌ 0 ┐ = I and, for every k, ┌ k + 1 ┐ = ⟨F, ┌ k ┐⟩
which is a rather convoluted and impractical way to represent natural numbers compared to the Church numerals Cn which iterate a given function n times on a giving argument.
There are cases where it makes sense to use tuples to represent natural numbers, namely to simplify the definition of predecessor, subtraction, and comparison. But that uses 1-tuples rather than 2-tuples [1].
Replacing Church numerals by tuple numerals allowed a googologically VERY large number (based on the so-called Bashicu Matrix System) to be expressed in only 350 bits rather than 404 bits. [2]
[1] https://github.com/tromp/AIT/blob/master/numerals/tuple_nume...
[2] https://github.com/tromp/AIT/blob/master/fast_growing_and_co...
So <a> is a function that applies its argument to a.
Peter Smith (logic God) also recommends it in his logic study guide:
I also had previously thought I wasn't that interest in formal proofs because I was never super interested in traditional mathematical proofs, but once I realize formal proofs can be viewed as an extension of type checking it got me a lot more interested!
¹ https://matthodges.com/posts/2022-07-17-exploring-lambda-cal...
Edit: now, if I could rename “lambda” as λ.
Lately, I was wondering about if it's possible to represent any logic by choosing a suitable base of combinators, and the sentences in the logic would correspond to beta-normal terms expressed in those combinators. What brought me to the idea is that we can represent certain substructural logics using a subset of B, C, K, W. Also, one can represent classical logic by using a different base than S and K, which allows for call/cc.
What would be intriguing, a choice of combinator base such that it could express terms in Church's typed lambda calculus. The composition of combinators would fail to normalize iff the corresponding composed term in typed lambda calculus failed to typecheck.
I think this could lead to somewhat simpler foundations of mathematics, instead of having types and various axioms, we would just say here's a base set of combinators and have fun combining them.
I had a hard time understanding his papers, you may have better luck.
https://www.cambridge.org/core/journals/journal-of-symbolic-...
My idea is different than introducing a new special combinator operator. Instead I want to formalize what a "question" is. In type theory, we can formalize any(?) mathematical question as a question of finding a term of a certain type. I want to replace that with a combinator equation Ax=B, where A and B are given lambda terms and x is an unknown. However, with x being any normalizable lambda term this wouldn't work, so I add additional condition that x must be what I call a "primitive term" (I haven't seen it defined anywhere sorry), expressible as a lambda term where only a given number of lambda abstractions occur in the front of the term and no other abstractions in its body, only applications. These are terms expressible in normal form as applications of only arguments, so many of the commonly used combinators are primitive (they don't compose though, for example, Y combinators are not primitive).
By choice of A, we can control the "combinator base" that x accepts inside the equation, so we can restrict the "type" of x that are solutions to the equation. So we can represent the question of y being of type T as a question of there being a primitive term x for an equation Ax=B (i.e. Ax and B both normalize to identical expression), where A and B is chosen based on T and y corresponds to x taking a chosen combinator base (the logic we work with) as arguments.
I was interested in formalizing what a question is, because I think that formalizing mathematics using type theory requires quite large meta-logical apparatus. However, using only untyped lambda calculus (and notion of beta-normalized equation with a primitive unknown) as a replacement for type theory is easy to embed into untyped lambda calculus itself using self-interpretation. The correspondence between the embedded language and the untyped lambda calculus (i.e. description how untyped lambda calculus manifests within the self-interpreter, and how questions are translated) could then be the only metalogical axiom required.
Bunder's papers are hard to find. It's been a while, but I think that "illiative" approach is precisely what Bunder tried to articulate. I recall one paper where he proved you could do set their with Combinator Logic and an "element of" operator. I think.
> The λ calculus is, at heart, a simple notation for functions and application.
I'm already confused! and application. Does that even make sense? It didn't get much better when I started on the first chapter. It seemed like an exercise in making simple algebra much more complicated, for philosophical reasons, or something.
I've no doubt at all that lambda calculus (whatever it is) is extremely important and valuable and if I put in the work and broke through the barriers I'd be embarrassed about my last paragraph.
But still, is there no way to introduce the subject in a slightly less obtuse and confusing way?
But I feel you. I'm sure there is a less academic way to explain this stuff.
Do you know Lisp or Clojure? Then you already understand lambda calculus.
Do you know JavaScript? Then replace all those lambdas with arrow functions:
(λ x . x + 2) 1
(x => x + 2)(1)
Like Turing machines, this is a general model for computation. But it's conceptually much simpler and easier to reason about mathematically.
Each computation step comes down to rewriting the program. That's just like computing algebraic expressions on paper:
(1 + 2)x - 2x
= 3x - 2x
= x
In the lambda calculus you can do the same but you have "applying a function" as a step that you can do:
(λ x . x + 2) 1
= 1 + 2
= 3In this case, we find after the abstract and the contents list that the idea is that a function is a general expression like x^2+1, with a variable x. Applying this function to an argument, e.g. 2, results in the value 5.
Edit: So that should make sense of the idea of a function, on one hand, and the application of the function, on the other.
The idea behind lambda calculus was to come up with a certain primitive set of operations that were precise enough that they could be defined mechanistically (and this was before the days when computers existed that could carry these out mechanistically), but also were rich enough that they could be used in combination to compute any function hitherto devised
Then I kind of recoiled from reforming, say f(x) = x^2 + 1 so f(1) = 1^2 + 1 = 2 into something seemingly more complicated for reasons that are difficult to discern for me as a reader and no doubt difficult to describe as an expert writer. I have the same difficulty with your last paragraph.
The reason things can seem more complicated than they need to be is that this set of primitive operations is so minimal; and the reason it's so minimal is that Alonzo Church came up with it in the 1930s when they were trying to get to the very bare bones of the concept of computation.
Lambda calculus is the grandfather of all functional programming languages. Lisp was a more or less direct implementation of it