These notes will recapitulate, make more precise, and to some degree expand what we did in the last hour of our first meeting, leading up to the definitions of the `factorial` and `length` functions.
+### Getting started ###
+
We begin with a decidable fragment of arithmetic. Our language has some primitive literal values:
0, 1, 2, 3, ...
As I mentioned in class, I will sometimes write ∀ x : ψ . φ in my informal metalanguage, where the ψ clause represents the quantifier's *restrictor*. Other people write this like `[`∀ x : ψ `]` φ, or in various other ways. My notation is meant to parallel the notation some linguists (for example, Heim & Kratzer) use in writing λ x : ψ . φ, where ψ clause restricts the range of arguments over which the function designated by the λ-expression is defined. Later we will see the colon used in a somewhat similar (but also somewhat different) way in our programming languages. But that's just foreshadowing.
+
+### Let and lambda ###
+
So we have bounded quantification as in ∀ `x < 10.` φ. Obviously we could also make sense of ∀ `x == 5.` φ in just the same way. This would evaluate φ but with the variable `x` now bound to the value `5`, ignoring whatever it may be bound to in broader contexts. I will express this idea in a more perspicuous vocabulary, like this: `let x be 5 in` φ. (I say `be` rather than `=` because, as I mentioned before, it's too easy for the `=` sign to get used for too many subtly different jobs.)
As one of you was quick to notice in class, though, when I shift to the `let`-vocabulary, I no longer restricted myself to just the case where φ evaluates to a boolean. I also permitted myself expressions like this:
means, too. It's just *the function* that waits for an argument and then returns the result of `x + 1` with `x` bound to that argument.
-*More to come.*
+This does take us beyond our (first-order) fragment of arithmetic, at least if we allow the bodies and arguments of λ-expressions to be any expressible value, including other λ-expressions. But we're having too much fun, so why should we hold back?
+
+So now we have a new kind of value our language can work with, alongside numbers and booleans. We now have function values, too. We can bind these function values to variables just like other values:
+
+`let id be` λ `x. x; y be id 5 in y`
+
+will evaluate to `5`. In reaching that result, the variable `id` was temporarily bound to the identity function, that expects an argument, binds it to the variable `x`, and then returns the result of evaluating `x` under that binding.
+
+This is what is going on, behind the scenes, with all the expressions like `succ` and `+` that I said could really be understood as variables. They have just been pre-bound to certain agreed-upon functions rather than others.
+
+
+### Containers ###
+
+*More coming*
+
+### Patterns ###
+
+*More coming*
+
+### Recursive let ###
+
+*More coming*
+
+### Comparing recursive-style and iterative-style definitions ###
+
+*More coming*
+
+