Tree @master (Download .tar.gz)
cpressey.md @master — view markup · raw · history · blame
Commentary by cpressey on Lambda Calculus works
The Calculi of Lambda-Conversion
Introduction to Combinators and the Lambda Calculus
Barendregt 1984 should be on this list but isn't. So, this is.
Appendix 3 (yes the appendices have numbers, not letters) is a humourous guide to "Care of your pet combinator".
A Short Introduction to the Lambda Calculus
A fixed-point combinator can be given (the Y combinator), but in the simply-typed lambda calculus, it cannot be given a type. Thus recursion cannot be done in the STLC and thus the STLC is not Turing-complete.
Introduction to Lambda Calculus
This is where I found out about Combinatory Reduction Systems from.
Chapter 5: The Untyped Lambda Calculus
Untyped Lambda Calculus
A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure
So one thing I haven't wrapped my head around here, is that this lambda calculus has abstractions that take a list of parameters, instead of one abstraction each; which is a lot more like a conventional programming language (with functions but no currying by default). And this is isomorphic to the sequent calculus? Does this mean anything?
The Lambda Calculus is Algebraic
"Yes, but what IS an indeterminate?"
It is algebraic in some sense, but probably not the sense I'd like it to be algebraic in.
(here are some older notes I had written about it)
The usual construction is to convert lambda calculus to combinatory logic and then, combinatory logic is algebraic. But there are weaknesses to this device, apparently.
The obscure Xi-rule that Selinger talks about
M = N implies λx.M = λx.N
is related to extensionality. Eta-conversion is there for extensionality. The conditions for extensionality are mentioned on this page:
https://cstheory.stackexchange.com/questions/8259/whats-the-point-of-eta-conversion-in-lambda-calculus
- for all λ-terms M and N, if Mx=Nx then M=N, or
- for all f,g if ∀x.fx=gx then f=g.
Not sure if 2 is right, because the Xi-rule is the converse of it.
Another answer there says this, which seems to explain it a bit better:
η-reduction captures the notion of extensionality - two functions are considered equal iff they give the same outputs on the same inputs.
One way of formalizing this notion is the following: if we consider the relation =βη, the transitive-reflexive closure of relation →βη, it is natural to characterize this relation in terms of inference rules of an equational theory (e.g.: rules of the form: if M=N, then λx.M=λx.N and so on - characterizing =β requires about 7 rules of this kind).
Now, replacing =β with =βη amounts to introducing the axiom λx.Mx=M, which is equivalent to the extensionality rule: if Mx=Nx, then M=N. This is exactly the notion that two functions equal on all input arguments should be considered identical.
Would be lovely to know what all the rules of =βη are.
Searching for "βη-equivalence" does return some hits, though not a lot of fertile ground.
A Lambda Calculus with Naive Substitution
This paper is cited in something else I read -- possibly "Equational Logic as a Programming Language".
I have read this paper, although maybe I missed the point when I did.
Basically, the substitution operator substitutes using a list of positions, rather than a name? This seems underwhelming.
A Graph-like Lambda Calculus for which Leftmost-Outermost Reduction is Optimal
I read this, but not entirely comprehendingly -- I could stand to read it again.
This paper is cited in "Equational Logic as a Programming Language".
Staples gives top-level rules for beta-reduction of the lambda calculus (after it has been converted to de Bruijn indexes) which are essentially algebraic-looking, and which resemble the S, K, I combinators:
(\x.x G) -> G
(\x.y G) -> y (where y =/= x)
(\x.(E F) G) -> ((\x.E G) (\x.F G))
(\x.\y.E G) -> (\y.(\x E G))
Which seems to imply that you can derive the S, K, I combinators from analyzing the lambda calculus algebraically.
Which seems weird, because I thought the S, K, I combinators came originally from (Schoenfinkel) taking that basic axiom system of Hilbert's and making them "point-free".
But weirder things have happened. So, OK.
On the Relation between the λμ-Calculus and the Syntactic Theory of Sequential Control
For a long time it has been widely thought that a classical proof, as opposed to an intuitionistic one, did not carry any computational content... but! Types-as-propositions.
I guess by "Syntactic Theory of Sequential Control" they refer to continuations.