lambda.rkt

#lang racket

;; CIS352 'S26 Lecture Notes -- Introduction to the Untyped λ-Calculus 

;; ☐ The Untyped λ-Calculus
;; ☐ β-reduction
;; ☐ λ-calculus Semantics and Normal Forms

;; Today we will learn about one of the most central aspects of the
;; course: Alonzo Church's untyped λ-calculus. The λ-calculus is not
;; at all like the integral calculus. Instead, the λ-calculus is a
;; computationally "complete" system consisting of an extremely
;; minimal number of syntax and semantic rules.

;; The syntax of the λ-calculus includes just three forms. We define
;; untyped λ-calculus expressions in the following manner:
;;
;;    e ∈ Expr ::=   (read: "The set Expr, of expressions consists of...")
;;              | x             <-- Variable references
;;              | (λ (x) e)     <-- λ abstractions
;;              | (e e)         <-- Application

;; That is the syntax of the λ-calculus. We will spend a long time
;; studying the "semantics" of the λ calculus: the untyped λ-calculus
;; has a fairly "nondeterministic" semantics defined in terms of
;; rewriting rules---to turn the λ calculus into a programming
;; language (such as Racket / Haskell / etc.), we will need to make
;; some more decisions (we will cover this in later classes).

;; For now, let's see some examples of λ-calculus terms:

;; λx. x, which I would write as... (λ (x) x)
;; λx. λy. x, which I would write as... (λ (x) (λ (y) x))
;; λx. x y, which I would write as... (λ (x) (x y))
;;
;; Notice that Racket's syntax completely disambiguates what is going
;; on, hence we will stick with the Scheme-style λ, compared to the
;; more traditional λ-calculus notation.

;; QuickAnswer

;; Which of the following (possibly multiple) is in the lambda calculus?
;;
;; (A) (λ (x) y)
;; (B) (λ (x y) x)
;; (C) (λ (x) (λ (y) (λ (z) (z x))))
;; (D) ((λ (x) e) 1)

;; ☐ β-reduction

;; β-reduction is the most fundamental operation in the λ calculus. It
;; simply means the following:
;;
;;     ((λ (x) e-b) e-a) β⟹ e-b [x ↦ e-a]
;;
;; In other words: any expression (e-f e-a) is a candidate for
;; β-reduction whenever `e-f` is of the form `(λ (x) e-b)`. We call
;; expressions of this form *redexes* for "reducible expressions."
;; 
;; The "meaning" of a λ-calculus term is given by all of the possible
;; different reductions (so far we have talked only about β) we can do
;; to it. Some cases are easy, let's see our first example of β
;; reduction:
;;
;;     ((λ (x) x) y) β⟹ x [x ↦ y] ≡ y
;; 
;; Notice how in this case, `y` is the argument. But we couldn't write
;; this in Racket:
;; 
;;   ((λ (x) x) y) <-- Syntax error: y is unbound variable
;; 
;; β-reduction, and the untyped λ-calculus in general, doesn't care
;; that the variable is unbound. β-reduction just says: "to apply a
;; function (λ (x) e-b) to an argument expression e-a, substitute x by
;; e-a in the body"

;; QuickAnswer
;; 
;; Perform β-reduction on the term `((λ (x) (x (x y))) z)`

;; QuickAnswer
;; 
;; Perform β-reduction on the term `((λ (x) (λ (y) (y x))) (λ (z) z))`

;; QuickAnswer
;; 
;; Perform β-reduction on the term `((λ (x) (x x)) (λ (x) (x x)))`

;; ☐ -- Substitution: Tricky, we will skip for now

;; One note: we are being colloquial about substitution. In fact,
;; substitution is a bit tricky, and it requires some care. We will
;; discuss these nuances in a future lecture, where we will cover some
;; other reduction rules and technical details. For now, it is
;; sufficient to say that you can intuit substitution as "plug and
;; chug" from grade-school algebra / calculus.

;; ☐ -- Reducing deep into a term
;; 
;; Sometimes, the redex will not be obvious. In fact, in general, a
;; term may have multiple redexes.
;; 

;; QuickAnswer
;;
;; Give a term that contains *two* redexes, i.e., two subexpressions
;; such that the expression could have β-reduction performed upon it.

;; In the untyped λ calculus, we typically construe β reduction to be
;; *any possible* beta reduction deep down within the term. Ultimately
;; we will see that this is not what we want for programming, but for
;; now we will develop it.
;; 
;; QuickAnswer
;; 
;; The following term has two possible β-reductions:
;; 
;; ```
;; ((λ (x) y)
;;  ((λ (z) (z z)) (λ (a) (a a))))
;; ```
;; 
;; Please perform both possible β reductions, what is the result?

;; ☐ -- λ-calculus Semantics and Normal Forms

;; We will see that, surprisingly, the λ-calculus is Turing
;; complete. This is surprising because, essentially, β-reduction is
;; the *only* computational rule in the whole system. There will be
;; some other reduction rules (α and η), which will have their own
;; place, but β is the main computational rule.

;; The λ-calculus is ruthlessly tiny, essentially the "assembly
;; language" of functional programming, stripping down functional
;; programming *just* to function calls.

;; The "semantics" of the untyped λ-calculus is defined by reduction
;; rules. We have seen one already: the β rule. We can see each
;; β-reduction as one "step" of computation in the λ-calculus. Most
;; interesting programs will take--in general--multiple steps of
;; β-reduction to reduce to a *normal form*.

;; [Definition, Normal Form] The term "normal form" refers to a class
;; of expressions which cannot be reduced any further
;; according to some metric. For example, in β-normal form, there can
;; be *no* unreduced β-reductions *anywhere* in the term.

;; QuickAnswer
;; 
;; Which of the following are in β-normal form:
;; 
;; (A) (λ (x) (λ (y) (x (λ (z) y))))
;; (B) (λ (x) ((λ (z) x) x))
;; (C) (z (λ (x) (x x)))
;; (D) (λ (x) (x ((λ (y) y) x)))

;; Fact: it is impossible, in general, to take an arbitrary λ-calculus
;; expression and determine whether a β-normal form exists.
;; 
;; Explanation: Equivalent to the halting problem.

;; So far, our lecture has focused on the definition of the λ-calculus
;; as a *term rewriting* system. In fact, this is precisely what the
;; λ-calculus is: a formulation of functions as terms, where we can
;; use β to drive computation via rewriting / substitution. 

;; When we imagine *computing* with the λ-calculus, we imagine running
;; *many* steps of β reduction, gradually reducing the term into a
;; *value* (i.e., result). Thus, we can see normal forms as *values*,
;; the results of fully-reducing an expression.

;; QuickAnswer
;; 
;; Fully-reduce the following term to β-normal form:
;; 
;;     (((λ (x) (λ (y) (x y))) (λ (x) x)) (λ (b) a))
;; 
;; Show each step of each β-reduction.

;; As we will see, the "meaning" of a λ-calculus term is a large,
;; non-deterministic tree of all possible ways in which it could
;; potentially be reduced. Some of these will yield normal forms, and
;; some of them will not.

;; QuickAnswer
;; 
;; Which of the following is true about the following term:
;;    ((λ (x) z) ((λ (x) (x x)) (λ (x) (x x))))
;; 
;; - (A) The term reduces forever
;; - (B) The term reduces to `z`
;; - (C) Both (A) and (B)

;; Summary: Day one of the λ-calculus
;; 
;; - A *calculus* refers to a system for manipulating and rewriting
;; terms. The differential and integral calculus is a system for
;; rewriting terms via symbolic differentiation/integration.
;; 
;; - The untyped λ-calculus is a system of computing with terms that
;; aims for absolute minimalism.
;; 
;; - Only three forms: variables, application, and λ-abstraction.
;; 
;; - The single computational rule is given by β, we will learn more
;; reduction rules soon but β is the main (compute-relevant) one.
;; 
;; - The "meaning" of a term in the λ-calculus is given by a reduction
;; relation (in this case we have learned only of β-reduction): the
;; idea is that the term will be reduced multiple times until it
;; reaches some "normal form."
;; 
;; - A normal form is when you can't reduce any further, by some
;; metric. We learned one normal form today: β-normal form, in which
;; there is no more β-reduction possible.
;; 
;; - In the untyped λ-calculus, a given term may have a multitude of
;; different possible redexes (reducible subexpressions). The untyped
;; λ-calculus does not tell us which of those redexes must be applied,
;; and so the meaning of a term in the λ-calculus may have some
;; ambiguity: all different possible ways of reducing the term.
;; 
;; - This leaves us with an obvious question: will all ways of
;; reducing the term reach the same conclusion / normal form? It turns
;; out the answer is Yes*, under some circumstances, which we will
;; learn about in the next lectures. In short: the Church-Rosser
;; theorem tells us that if a term *does* have a normal form, it will
;; be unique up to variable renaming.
;; 
;; Church wasn’t trying to model hardware. He was trying to:
;; - Characterize effective calculability
;; - Provide a logical foundation for mathematics
;; - β-reduction was a mathematical equality principle, not an execution model.