Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Lambda Calculus

The Calculi of Lambda-Conversion

• rating: classic

.

Introduction to Combinators and the Lambda Calculus

• rating: TODO

Barendregt 1984 should be on this list but isn't. So, this is.

A Short Introduction to the Lambda Calculus

• rating: 2

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

• rating: 2

This is where I found out about Combinatory Reduction Systems from.

Chapter 5: The Untyped Lambda Calculus

• rating: 2

.

Untyped Lambda Calculus

• rating: 1

.

A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure

• rating: 1

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

• rating: 3

"Yes, but what IS an indeterminate?"

A Lambda Calculus with Naive Substitution

• rating: 0

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

• rating: 1

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

• rating: TODO

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.

functional programming - Is Lambda Calculus purely syntactic? - Computer Science Stack Exchange

• rating: 1

.

What are the axioms, inference rules, and (formal) semantics of lambda calculus? - Computer Science Stack Exchange

• rating: 1

.

lo.logic - What\'s the point of \$\eta\$-conversion in lambda calculus? - Theoretical Computer Science Stack Exchange

• rating: 1

.

lambda calculus - What\'s the definition of equational theory? Why is λ logic free? - Mathematics Stack Exchange

• rating: 1

.

lo.logic - Scott on the consistency of the lambda calculus - MathOverflow

• rating: 1

.

Lambda Terms

• rating: TODO

.

The largest number representable in 64 bits

• rating: 1

.

lo.logic - What\'t the smallest lambda calculus term which is not known to have a normal form? - MathOverflow

• rating: 1

.

maciej-bendkowski/lambda-sampler: Boltzmann sampler utilities for lambda calculus

• rating: 1

.