help with "Type Theory & Formal Proof" ex 3.5a on λ2

Stream: new members

[rzeta0]

I'm a beginner who, in an attempt to lean how proof assistants like Lean work, started working through "Type Theory & Formal Proof" (book) - based on a suggestion here a few months ago.

Chapter 1 introduces untyped lambda calculus. Chapter 2 introduced simply typed lambda calculus, and Chapter 3 briefly introduces second order lambda calculus - specifically the type-binder $\Pi$ vs the normal binder $\lambda$.

---

Exercise

I've done all the exercises so far but am now stuck on Chapter 3 Ex 5 (a)

As stated, the exercise is:

Let $⊥≡Πα : ∗. α$ and $Γ ≡β : ∗, x : ⊥$.
(a) Prove that $⊥$ is legal.

A term $T$ is legal in this textbook if there exists a context $Γ$ and type $ρ$ such that $Γ⊢T:ρ$.

However the errata on the author's web page (end of this pdf) says

Page 82, Exercise 3.5 (a): The notion ‘legality’ has not yet been defined.
Read this part of the exercise as:
Show that there is a $t$ such that $⊥: t$.

---

My thoughts

My initial thought is that $⊥≡Πα : ∗. α$ is a type and therefore doesn't belong on the left hand side of a colon. This suggest the errata itself is in error! This is also the view of someone else who replied on SE.

If, as someone on SE, suggested, the exercise should be

Show that there is a $t$ such that $t:⊥$.

that might make more sense to me.

I then tried to "read" the expression $⊥≡Πα : ∗. α$ to see its semantics might give a clue. I read it as "the type of things that take a type as input and output a thing of that type" - type → object. This is new to me. I'm used to "things that take objects of a given type and output things of a given type" - object → object.

I tried to create such a term,

$$λα:*.x:α \quad : \quad \Pi α:* . α$$

but this, I'm told, is not valid as $x$ is unbound.

The textbook itself provides a worked example where all variables are bound.

$$λα : ∗. λf : α →α. λx : α. f(fx) : Πα : ∗. (α →α) →α →α.$$

---

I'd welcome guidance, especially if it is aimed at a self-teaching beginner (me!).

[Aaron Liu]

I don't think there is a $t$ such that $t : \bot$. To me $\bot$ looks like one of the standard encodings of an empty type.

[Aaron Liu]

However, I'm not very familiar with the notation so I could be wrong.

[rzeta0]

Hi Aaron, the author hasn't introduced $⊥$ with any special meaning yet. I assume that might happen later.

[Aaron Liu]

After reading a little, why not $\bot : *$?

[rzeta0]

Interesting - let me think about it.

My initial thought is that the "type of a type" has to go up the ladder one step. I believe some people call the step up from types "sorts" or "universes". However, the author hasn't introduced any of that yet.

If what you say is correct, then the type of a type would also be a type at the same level. Is this right?

[Aaron Liu]

Yes, this is called impredicativity

[rzeta0]

OK - the author did mention "impredicativity" in the further reading at the end of chapter 3 so this might be the thread I need to pull on. Thanks.

[Dan Velleman]

Can you use the Formation rule (Definition 3.4.7 on p. 76)?

[rzeta0]

hi Dan, I've already been staring at the $(abst_2)$ rule and can't see how it might help.

Let me elaborate my thinking.

The $(abst_2)$ rule is the only one of the derivation rules that has a type-binder $\Pi$ in its conclusion, so is worth exploring.

$$(abst_2) \quad \frac{Γ, α : ∗ \quad ⊢ \quad M : A}{Γ \quad ⊢ \quad λα : ∗. M : Πα : ∗. A}$$

Here we want $A\equiv \alpha$. That means $M$ has type $\alpha$. That means the context $Γ$ must contain $M:\alpha$.

Let's try $M:\alpha \equiv x:\alpha$. Sadly when I try it in the rule it breaks:

$$(abst_2) \quad \frac{α : ∗ , x:\alpha \quad ⊢ \quad x : \alpha}{x:\alpha \quad ⊢ \quad λα : ∗. x : Πα : ∗. \alpha}$$

Here the top (premise) looks ok if we don't worry about the order of declarations in the context, as per the textbook. But the bottom (conclusion) looks wrong because we know nothing about $\alpha$ in the context, but seem to make an entailment from it.

I should say I am not sure of myself about this - I'd welcome guidance.

[Aaron Liu]

Your context doesn't seem to be ordered correctly. $x : \alpha$ should go after $\alpha : *$ since $x$ depends on $\alpha$.

[rzeta0]

hi Aaron - I've updated to change the order.

[Aaron Liu]

rzeta0 said:

Here the top (premise) looks ok if we don't worry about the order of declarations in the context, as per the textbook.

I think this time you do have to worry about the order, since if you mess with the order you can break the context.

[Aaron Liu]

For example as you have observed $\alpha : *, x : \alpha$ is a valid context but $x : \alpha, \alpha : *$ is not.

[Aaron Liu]

So to apply the $(abst_2)$ rule you have to reorder the context to place $\alpha : *$ at the right, but you can't do this since $x$ depends on $\alpha$.

[Aaron Liu]

From section 3.6, at the bottom of page 79:

Note that the only lemma from Chapter 2 that we have to adapt is the Permutation Lemma (cf. Lemma 2.10.5): it is no longer allowed to arbitrarily permute the declarations in a context $\Gamma$ occurring in a judgement $\Gamma \vdash M : T$, since a declaration occurring later in that context may depend on an earlier one, as we have explained in Section 3.4. If we require, however, that the permuted context is a $\lambda2$-context, again, then it holds.

[Dan Velleman]

I would follow the errata: Show that there is a $t$ such that $\bot : t$.
And to do that I would use (form).

[rzeta0]

@Dan Velleman - my apologies, I mistook your reference to (form) as meaning the table of derivation rules Fig 3.1.

I will look at this afresh tomorrow after some sleep.

[Mario Carneiro]

@rzeta0 I'm quite sure that is what Dan means

[Mario Carneiro]

I don't have the book but from the solutions pdf I'm guessing it says something like:

$$(form) \quad \frac{Γ ⊢ α : \square \quad Γ, x : α ⊢ \beta : \square}{Γ ⊢ Πx : α. \beta : \square}$$

[rzeta0]

@Mario Carneiro The formation rule is, to quote the book:

Definition 3.4.7 (Formation rule)
(form) Γ ⊢ B : ∗ if Γ is a λ2-context, B ∈T2 and all free type variables in B are declared in Γ.

This is required in order to enable the use of (appl2) rule

$$(appl_2) \quad \frac{Γ ⊢ M : (Πα : ∗. A) \quad Γ ⊢ B : ∗}{Γ ⊢ MB : A[α := B]}$$

Without the formation rule, there is no other rule that gives us $B:*$.

[Aaron Liu]

So then (form) would derive $\vdash (\Pi \alpha : * . \alpha) : *$, since the empty context is a valid context and $\Pi \alpha : * . \alpha$ is a valid term that has no free variables that need to be in the context, right?

[Mario Carneiro]

the application rule is a red herring, just focus on the (form) rule itself