View Source Document

Chris Pressey.md

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

.

Introduction to Combinators and the Lambda Calculus

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

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?"

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.

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

.

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

.

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

.

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

.

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

.

Lambda Terms

.

The largest number representable in 64 bits

.

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

.

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

.