<p>I think your <code>neutral-bad</code> lemma is too general. For instance:</p>
<p><span class="math-container">$$f : τ ⇒ σ, x : τ ⊢ f\ x : σ$$</span></p>
<p><span class="math-container">$σ$</span> does not occur in the context, but there is a neutral term with its type.</p>
<p>However, that is not the situation you're going to end up in. I believe where you'll end up is:</p>
<p><span class="math-container">$$s : ι ⇒ ι, z : ι ⊢ F\ X \ Y : ι$$</span></p>
<p>where <span class="math-container">$F$</span> must be a neutral term with type <span class="math-container">$σ ⇒ τ ⇒ ι$</span>. But now you can prove there are no neutral terms in that context whose type is of the form <span class="math-container">$σ ⇒ τ ⇒ ε$</span>.</p>

CC BY-SA 4.0
2024-04-18T12:46:33.130Z
Right, I thought of defining that lemma on the context restricted to the term, but then I may still find issues because my contexts, being lists, have order.
I'll try to use the type's length to show it's not in the context. Thank you!
lfrg
CC BY-SA 4.0
2024-04-18T21:14:25.773Z
Thinking about your example :τ⇒σ,:τ⊢ :σ, maybe I should focus on the subterms instead?
lfrg
CC BY-SA 4.0
2024-04-18T21:54:50.657Z
I'm not sure what a general version of the lemma you need is. But, I was able to define a version of your $\mathsf{Ne} → ℕ$ myself, and what I wrote was part of my argument. Any neutral function that isn't a reference to the context can only come from the application of a function with a larger type. So if you are larger than any type in the context, that leads to an infinite regress.
Dan Doel
CC BY-SA 4.0
2024-04-19T02:37:19.830Z
It worked indeed, thank you very much!
lfrg
CC BY-SA 4.0
2024-04-18T05:13:29.490Z
2024-04-18T05:13:29.490Z
Dan Doel
<p>Beginer here. I'm trying to show that the closed <span class="math-container">$\beta$</span>-nf's of type <span class="math-container">$ (\iota \to \iota) \to (\iota \to \iota) $</span> are the Church numerals (<span class="math-container">$\iota$</span> the base type, using the simply-typed lambda calculus).</p>
<p>In Hindley's Basic Simple Type Theory, the lemma 8A5 states that every <span class="math-container">$\beta$</span>-nf can be expressed uniquely in the following form (types omitted):
<span class="math-container">$$ M \equiv \lambda x_1 . .. x_m \cdot (\nu M_1... M_n) $$</span>
Where <span class="math-container">$ m \ge 0 $</span>, <span class="math-container">$ n \ge 0$</span>, and the type <span class="math-container">$ \tau $</span> of <span class="math-container">$ M $</span> is
<span class="math-container">$ \tau \equiv \tau_1 \to ... \to \tau_m \to \tau^* $</span>. And each <span class="math-container">$M_j$</span> is a <span class="math-container">$\beta$</span>-nf, too. And if <span class="math-container">$M$</span> is closed then <span class="math-container">$ m \ge 1 $</span> and <span class="math-container">$ \nu $</span> is one of the <span class="math-container">$x_i$</span>'s.</p>
<p>Now, it is easy to show (informally) that the (long) normal inhabitants of the type <span class="math-container">$ (\iota \to \iota) \to (\iota \to \iota) $</span> are exactly the Church numerals, but I'm struggling to formalise that in Agda.</p>
<p>I follow the common definition of normal terms found in the literature, something like:</p>
<pre><code>mutual
  data Nf : Context → Type → Set where
    ne  : {Γ : Context} → Ne Γ ι → Nf Γ ι
    abs : {Γ : Context} {σ τ : Type} → Nf (Γ ∷ σ) τ → Nf Γ (σ ⇒ τ)

  data Ne : Context → Type → Set where
    var : {Γ : Context} {σ : Type} → Γ ∋ σ → Ne Γ σ
    app : {Γ : Context} {σ τ : Type} → Ne Γ (σ ⇒ τ) → Nf Γ σ → Ne Γ τ
</code></pre>
<p>Where the <code>Context</code> is a list of <code>Type</code>'s, and we use de Bruijn indices for variables.</p>
<p>I get stuck when I case split on the head of the term (it is a <code>Ne</code>), because <code>app</code> introduces a term of a new type which I don't know how to relate to any of the types in the context. Here's a naive function to clarify what I mean:</p>
<pre><code>naive : Nf ∅ ((ι ⇒ ι) ⇒ (ι ⇒ ι)) → ℕ
naive (abs abs (ne (var Z))) = zero
naive (abs abs (ne (var S S () )))
naive (abs abs (ne (app (var S Z) N))) = suc ? -- This is the case I'm interested in
naive (abs abs (ne (app (app _ _) N))) = ? -- This is what I mean, think it's nonsense
</code></pre>
<p>I believe what I'm missing is a proof that <em>if <span class="math-container">$M$</span> is closed then [...] <span class="math-container">$ \nu $</span> is one of the <span class="math-container">$x_i$</span>'s</em>, so I'm trying to prove that a neutral term of a type not present in the context is not well-defined. Here's one attempt:</p>
<pre><code>neutral-bad : {Γ : Context} {σ : Type} → Ne Γ σ → σ ∉ Γ → ⊥
neutral-bad (var x)   not-there = ? -- Easy
neutral-bad (app r M) not-there = ? -- Stuck again
</code></pre>
<p>The proposition <code>σ ∉ Γ</code> above is defined with <code>Data.List.Relation.Unary.Any</code> and negation (maybe not relevant, but would rather make it clear anyway).</p>
<p>Can someone provide advise on how to solve this? or maybe point me to related works? All help is much appreciated!</p>

<type-theory><typed-lambda-calculus><agda>
Formalising Church numerals in Agda
lfrg
# Formalising Church numerals in Agda

(Asked by: username_0 on 2024-04-18)

Beginer here. I'm trying to show that the closed $\beta$-nf's of type $ (\iota \to \iota) \to (\iota \to \iota) $ are the Church numerals ($\iota$ the base type, using the simply-typed lambda calculus).
In Hindley's Basic Simple Type Theory, the lemma 8A5 states that every $\beta$-nf can be expressed uniquely in the following form (types omitted):
$$ M \equiv \lambda x_1 . .. x_m \cdot (\nu M_1... M_n) $$
Where $ m \ge 0 $, $ n \ge 0$, and the type $ \tau $ of $ M $ is
$ \tau \equiv \tau_1 \to ... \to \tau_m \to \tau^* $. And each $M_j$ is a $\beta$-nf, too. And if $M$ is closed then $ m \ge 1 $ and $ \nu $ is one of the $x_i$'s.
Now, it is easy to show (informally) that the (long) normal inhabitants of the type $ (\iota \to \iota) \to (\iota \to \iota) $ are exactly the Church numerals, but I'm struggling to formalise that in Agda.
I follow the common definition of normal terms found in the literature, something like:
mutual
  data Nf : Context → Type → Set where
    ne  : {Γ : Context} → Ne Γ ι → Nf Γ ι
    abs : {Γ : Context} {σ τ : Type} → Nf (Γ ∷ σ) τ → Nf Γ (σ ⇒ τ)

  data Ne : Context → Type → Set where
    var : {Γ : Context} {σ : Type} → Γ ∋ σ → Ne Γ σ
    app : {Γ : Context} {σ τ : Type} → Ne Γ (σ ⇒ τ) → Nf Γ σ → Ne Γ τ

Where the Context is a list of Type's, and we use de Bruijn indices for variables.
I get stuck when I case split on the head of the term (it is a Ne), because app introduces a term of a new type which I don't know how to relate to any of the types in the context. Here's a naive function to clarify what I mean:
naive : Nf ∅ ((ι ⇒ ι) ⇒ (ι ⇒ ι)) → ℕ
naive (abs abs (ne (var Z))) = zero
naive (abs abs (ne (var S S () )))
naive (abs abs (ne (app (var S Z) N))) = suc ? -- This is the case I'm interested in
naive (abs abs (ne (app (app _ _) N))) = ? -- This is what I mean, think it's nonsense

I believe what I'm missing is a proof that if $M$ is closed then [...] $ \nu $ is one of the $x_i$'s, so I'm trying to prove that a neutral term of a type not present in the context is not well-defined. Here's one attempt:
neutral-bad : {Γ : Context} {σ : Type} → Ne Γ σ → σ ∉ Γ → ⊥
neutral-bad (var x)   not-there = ? -- Easy
neutral-bad (app r M) not-there = ? -- Stuck again

The proposition σ ∉ Γ above is defined with Data.List.Relation.Unary.Any and negation (maybe not relevant, but would rather make it clear anyway).
Can someone provide advise on how to solve this? or maybe point me to related works? All help is much appreciated!

**Tags:** type-theory, typed-lambda-calculus, agda

---

## 1 answers

### Answer by username_1 on 2024-04-18. Score: 1 | Accepted answer

I think your `neutral-bad` lemma is too general. For instance:

$$f : τ ⇒ σ, x : τ ⊢ f\ x : σ$$

$σ$ does not occur in the context, but there is a neutral term with its type.

However, that is not the situation you're going to end up in. I believe where you'll end up is:

$$s : ι ⇒ ι, z : ι ⊢ F\ X \ Y : ι$$

where $F$ must be a neutral term with type $σ ⇒ τ ⇒ ι$. But now you can prove there are no neutral terms in that context whose type is of the form $σ ⇒ τ ⇒ ε$.

> **Comments:**
> **username_0**: Right, I thought of defining that lemma on the context restricted to the term, but then I may still find issues because my contexts, being lists, have order. I'll try to use the type's length to show it's not in the context. Thank you!  
> **username_0**: Thinking about your example :τ⇒σ,:τ⊢ :σ, maybe I should focus on the subterms instead?  
> **username_1**: I'm not sure what a general version of the lemma you need is. But, I was able to define a version of your $\mathsf{Ne} → ℕ$ myself, and what I wrote was part of my argument. Any neutral function that isn't a reference to the context can only come from the application of a function with a larger type. So if you are larger than any type in the context, that leads to an infinite regress.  
> **username_0**: It worked indeed, thank you very much!  

---

