# λ calculus

## Typed λ Calculus Interpreter in Agda

In a recent meeting I talked to my assistants about using dependent type to guarantee that, in an evaluator for λ calculus using de Bruin indices, that variable look-up always succeeds.

## S Combinator is Injective, with Proofs

By chance, I came upon a blog entry by Masahiro Sakai (酒井政裕) in which he, after reading my short comment “Do you know that the `S` combinator is injective?”, tried to construct the inverse of `S` and showed that `S⁻¹ ○ S = id` in, guess what, Agda!

## Encoding Inductive and Coinductive Types in Polymorphic Lambda Calculus

An indcutive type μF is simulated by ` forall x . (F x -> x) -> x`, while a coinductive type νF is simulatd by ` exists x . (x -> F x, x)`. When they coincide, we can build hylomorphisms, but also introduces non-termination into the language.

## Substraction not Definable in Simply Typed Lambda Calculus

We can even define primitive recursion, only that it does not have the desired type `primrec :: (N -> b -> b) -> b -> N -> b`. Therefore, predecessor does not get the type `pred :: N a -> N a` either.

## S Combinator is Injective

Do you know that the S combinator is injective? I have a simple algebraic proof and Nakano actually constructed its inverse.