OCaml (imperative part) untyped lambda calculus

-combinatorial logic +combinatory logic --------------------------------------------------- Turing complete --------------------------------------------------- @@ -191,7 +191,7 @@ Scheme (imperative part)

OCaml (imperative part) untyped lambda calculus

-combinatorial logic +combinatory logic --------------------------------------------------- Turing complete --------------------------------------------------- diff --git a/content.mdwn b/content.mdwn index d725c61c..aaab7a51 100644 --- a/content.mdwn +++ b/content.mdwn @@ -57,7 +57,7 @@ Week 3: * More on Lists Introduces list comprehensions, discusses how to get the `tail` of lists in the Lambda Calculus -* [[Combinatorial Logic|topics/week3 combinatory logic]] +* [[Combinatory Logic|topics/week3 combinatory logic]] * Reduction Strategies and Normal Forms * Homework for week 3 diff --git a/exercises/assignment3.mdwn b/exercises/assignment3.mdwn index 674cf40e..95450217 100644 --- a/exercises/assignment3.mdwn +++ b/exercises/assignment3.mdwn @@ -40,7 +40,7 @@ where `one` abbreviates `succ zero`, and `two` abbreviates `succ (succ zero)`. You'll need to make use of the predecessor function, but it's not essential to understanding this problem that you have successfully implemented it yet. You can treat it as a black box. -## Combinatorial Logic +## Combinatory Logic Reduce the following forms, if possible: @@ -53,7 +53,7 @@ Reduce the following forms, if possible: -16. Give Combinatorial Logic combinators (that is, expressed in terms of `S`, `K`, and `I`) that behave like our boolean functions. You'll need combinators for `true`, `false`, `neg`, `and`, `or`, and `xor`. +16. Give Combinatory Logic combinators (that is, expressed in terms of `S`, `K`, and `I`) that behave like our boolean functions. You'll need combinators for `true`, `false`, `neg`, `and`, `or`, and `xor`. Using the mapping specified in this week's notes, translate the following lambda terms into combinatory logic: diff --git a/index.mdwn b/index.mdwn index 5bddb85b..9fd9d69d 100644 --- a/index.mdwn +++ b/index.mdwn @@ -103,7 +103,7 @@ The [[differences between our made-up language and Scheme, OCaml, and Haskell|ro (**Week 3**) Thursday 12 February 2015 > Topics: More on Lists (in progress); -Combinatorial Logic (in progress); +Combinatory Logic (in progress); Reduction Strategies and Normal Forms (in progress); Homework (in progress) diff --git a/overview.mdwn b/overview.mdwn index d3909644..d90768af 100644 --- a/overview.mdwn +++ b/overview.mdwn @@ -5,7 +5,7 @@ This page aims to summarize the major "topics" (bits of conceptual technology) t * Basics of (especially "functional"-style) programming: including pattern matching, recursive definitions, abstract datatypes, **modularity, separating interfaces from implementation** * The syntax and proof theory of the untyped lambda calculus; at least some discussion of its semantics * Different **evaluation-order strategies** for formal systems, different "normalizing" properties -* Combinatorial logic, or the dispensability of variables +* Combinatory logic, or the dispensability of variables * Recursive definitions and recursive types, fixed-point combinators * Other **type sophistication**: abstract datatypes, polymorphic types, perhaps dependent types * **Mutation** and imperative/iterative idioms @@ -45,7 +45,7 @@ discussing this in much more detail as the course proceeds. The logical systems we'll be looking at include: * the so-called "pure" or untyped (monotyped?) lambda calculus -* combinatorial logic +* combinatory logic * the simply-typed lambda calculus * polymorphic types with System F diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn index 761bc775..f0b28cd7 100644 --- a/topics/week3_combinatory_logic.mdwn +++ b/topics/week3_combinatory_logic.mdwn @@ -1,5 +1,5 @@ -Combinators and Combinatorial Logic -=================================== +Combinators and Combinatory Logic +================================= Combinatory logic is of interest here in part because it provides a useful computational system that is equivalent to the lambda calculus, @@ -173,7 +173,7 @@ The fifth rule deals with an abstract whose body is an application: the S combin [Fussy notes: if the original lambda term has free variables in it, so will the combinatory logic translation. Feel free to worry about this, though you should be confident that it makes sense. You should also convince yourself that if the original lambda term contains no free variables---i.e., is a combinator---then the translation will consist only of S, K, and I (plus parentheses). One other detail: this translation algorithm builds expressions that combine lambdas with combinators. For instance, the translation of our boolean false `\x.\y.y` is `[\x[\y.y]] = [\x.I] = KI`. In the intermediate stage, we have `\x.I`, which mixes combinators in the body of a lambda abstract. It's possible to avoid this if you want to, but it takes some careful thought. See, e.g., Barendregt 1984, page 156.] -[Various, slightly differing translation schemes from combinatorial +[Various, slightly differing translation schemes from combinatory logic to the lambda calculus are also possible. These generate different metatheoretical correspondences between the two calculii. Consult Hindley and Seldin for details. Also, note that the @@ -271,7 +271,7 @@ and the S and K combinators is that the axioms correspond to type schemas for the combinators. Thsi will become more clear once we have a theory of types in view. -Here's more to read about combinatorial logic. +Here's more to read about combinatory logic. Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]]. Other sources include -- 2.11.0