proof theory as having just one rule, called the rule of **beta-reduction** or
"beta-contraction". Suppose you have some expression of the form:
- ((\ a M) N)
+ ((\a M) N)
that is, an application of an abstract to some other expression. This compound form is called a **redex**, meaning it's a "beta-reducible expression." `(\a M)` is called the **head** of the redex; `N` is called the **argument**, and `M` is called the **body**.
It's often said that dynamic systems are distinguished because they are the ones in which **order matters**. However, there are many ways in which order can matter. If we have a trivalent boolean system, for example---easily had in a purely functional calculus---we might choose to give a truth-table like this for "and":
true and true = true
- true and true = true
true and * = *
true and false = false
* and true = *
(let* [(bar (lambda (x) B))] M)
- then wherever `bar` occurs in `M` (and isn't rebound by a more local "let" or "lambda"), it will be interpreted as the function `(lambda (x) B)`.
+ then wherever `bar` occurs in `M` (and isn't rebound by a more local `let` or `lambda`), it will be interpreted as the function `(lambda (x) B)`.
Similarly, in OCaml:
let x = A;;
... rest of the file or interactive session ...
- It's easy to be lulled into thinking this is a kind of imperative construction. *But it's not!* It's really just a shorthand for the compound "let"-expressions we've already been looking at, taking the maximum syntactically permissible scope. (Compare the "dot" convention in the lambda calculus, discussed above.)
+ It's easy to be lulled into thinking this is a kind of imperative construction. *But it's not!* It's really just a shorthand for the compound `let`-expressions we've already been looking at, taking the maximum syntactically permissible scope. (Compare the "dot" convention in the lambda calculus, discussed above.)
9. Some shorthand
(define foo B)
(foo 2)
-don't involve any changes or sequencing in the sense we're trying to identify. As we said, these programs are just syntactic variants of (single) compound syntactic structures involving "let"s and "lambda"s.
+don't involve any changes or sequencing in the sense we're trying to identify. As we said, these programs are just syntactic variants of (single) compound syntactic structures involving `let`s and `lambda`s.
Since Scheme and OCaml also do permit imperatival constructions, they do have syntax for genuine sequencing. In Scheme it looks like this:
-1. Declarative vs imperatival models of computation.
-2. Variety of ways in which "order can matter."
-3. Variety of meanings for "dynamic."
-4. Schoenfinkel, Curry, Church: a brief history
-5. Functions as "first-class values"
-6. "Curried" functions
-
-1. Beta reduction
-1. Encoding pairs (and triples and ...)
-1. Encoding booleans
-
-
-
-
-