Learning about pure type systems

There is plenty written about pure type systems. People on ##dependent Freenode IRC channel knew to point out where to start looking from.

  1. Henk Barendgredt: Lambda calculi with types
  2. Antonius J.C. Hurkens: A Simplification of Girard's Paradox

Barendgredt's paper

Henk Barengredt's paper is helpful for understanding lambda calculus. λ-calculus is easily only treated as a computational system, but the equational meaning would be more important to understand.

Understanding of fixed-point theorem helps in recognizing how the y-combinator spoils the equational meaning in λ-calculus. The Corollary 2.1.10 points out that you can make any two lambda calculus expressions equivalent by using the fixed-point combinator.

I didn't understand Church-Rosser theorem after reading Barengredt's work.

The description of Curry's typing of lambda calculus helps in understanding illative combinatory logic.

Consistency

A type theory is consistent only if not every type is inhabited. It's not, if you can take a fixed-point combinator and use it to produce a program that inhabits a type.

If you are not careful and understand how to provide a consistency proof, you may inadvertedly break the consistency of typed lambda calculus.

Type:Type

The PTS allows you to define your own axioms and product rules. The system λ* can be easily shown to be inconsistent. The SAR-tuple for λ* is populated in the following way:

S = {*}
A = {*:*}
R = {(*,*,*)}

The following type can be produced from the given rules:

(∏_:*. *) : *

It allows to type the ω -combinator, and therefore Y -combinator as well.

ω = (λx.x x):(∏x:(* → *). *):*

half_Y = (λa.λf.λx.f(x x)):(∏a:*.∏f:(a → a).∏x:(* → a). a)

Y = (λa.λf.(λx.f(x x))(λx.f(x x))):(∏a:*.∏f:(a → a).a)

You may also simply prove that every type is inhabited:

(λa.(λx.(x x))(λx.(x x))):(∏a:*.a)

Girard's paradox & Hurkens' paper

Girard's paradox shows that simply extending sorts from the systems described by the lambda cube allows inconsistencies, even if you didn't bring it down to λ*.

The proof is not simple and I didn't understand it even after reading Hurkens' paper.

It appears that the problem is solved by cumulative type universes.

S = {Type n | n ∈ N}
A = {(Type n:Type (n+1)) | n ∈ N}
R = {(Type n, Type m, Type max(n,m)) | n,m ∈ N}

This is from "Parametricity and dependent types" -paper. It also shows how to translate this kind of a PTS into relational statements about inhabitants of the type. I don't understand the significance of it yet.

In such system we can no longer use the earlier expression to prove (λx.x x), because we can no longer pass (*0 → *0) : *1 into itself.

Strong normalization

I didn't get to finish with understanding strong normalization. I heard about logical relations and how you'd get to prove things with formation rules of lambda calculus, if you want to prove that the logic itself holds some properties.

To learn about logical relations, I'm about to watch Amal Ahmed's OPLSS lectures.

Similar posts