## 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.

Skip to content
# λ calculus

## Typed λ Calculus Interpreter in Agda

## S Combinator is Injective, with Proofs

## Encoding Inductive and Coinductive Types in Polymorphic Lambda Calculus

## Substraction not Definable in Simply Typed Lambda Calculus

## S Combinator is Injective

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.

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!

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.

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.

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