<p>In Girard <em>Proofs and Types</em>, The degree of a type is defined as follows</p>
<p><span class="math-container">$$\begin{align*}\partial(T_i)&amp;=1\text{ if }T_i\text{ is atomic}\\\partial(U\times V)=\partial(U\rightarrow V) &amp;=\max(\partial(U), \partial(V))+1\end{align*}$$</span></p>
<p>I interpret this as corresponding to one more than the length of the longest path in a directed graph.</p>
<p><a href="https://i.sstatic.net/34A7b.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/34A7b.png" alt="enter image description here" /></a></p>
<p>It defines the degree of a redex as <span class="math-container">$$\begin{align*}\partial(\pi^1\left&lt;u, v\right&gt;)=\partial(\pi^2\left&lt;u, v\right&gt;)&amp;=\partial(U\times V) \text{ where }U\times V\text{ is the type of }\left&lt;u, v\right&gt;\\\partial((\lambda x. v)u)&amp;=\partial(U\rightarrow V)\text{ where }U\rightarrow V\text{ is the type of }(\lambda x. v)\end{align*}$$</span> where <span class="math-container">$\pi^1$</span> and <span class="math-container">$\pi^2$</span> refer to the first and second projections of a pair with <span class="math-container">$\pi^1 \left&lt;u, v\right&gt; \rightsquigarrow u$</span> and <span class="math-container">$\pi^2 \left&lt;u, v\right&gt; \rightsquigarrow v$</span></p>
<p>It then continues to say</p>
<blockquote>
<p>The degree <span class="math-container">$d(t)$</span> of a term is the sup of the degrees of the redexes it contains. By convention, a normal term (i.e. one containing no redex) has degree 0.</p>
<p>NB: A redex <span class="math-container">$r$</span> has two degrees: one as a redex, another as a term, for the redex may contain others; the second degree is greater than or equal to the first: <span class="math-container">$\partial(r)\leq d(r)$</span></p>
</blockquote>
<p>I'm not sure how to interpret the definitions for the degrees of terms and redexes.</p>
<p>From my current understanding, if <span class="math-container">$u$</span> is a term of type <span class="math-container">$U$</span> and <span class="math-container">$v$</span> is a term with type <span class="math-container">$V$</span> then <span class="math-container">$\partial(\pi^1\left&lt;u, v\right&gt;)=2$</span> and <span class="math-container">$\partial(\pi^1\left&lt;\pi^1\left&lt;u, v\right&gt;, \pi^2\left&lt;u, v\right&gt;\right&gt;)=2$</span> as the type of <span class="math-container">$\left&lt;\pi^1\left&lt;u, v\right&gt;, \pi^2\left&lt;u, v\right&gt;\right&gt;$</span> is again <span class="math-container">$U \times V$</span> and <span class="math-container">$d(\pi^1\left&lt;\pi^1\left&lt;u, v\right&gt;, \pi^2\left&lt;u, v\right&gt;\right&gt;)=2$</span> as all the redexes have degree 2.</p>
<p>For the same reason, I also think <span class="math-container">$\partial(\pi^1\left&lt;\pi^1\left&lt;\pi^1\left&lt;u, v\right&gt;, \pi^2\left&lt;u, v\right&gt;\right&gt;, \pi^2\left&lt;\pi^1\left&lt;u, v\right&gt;, \pi^2\left&lt;u, v\right&gt;\right&gt;\right&gt;)=2$</span> but <span class="math-container">$\partial(\pi^1\left&lt;\left&lt;u, v\right&gt;, v\right&gt;)=3$</span> as <span class="math-container">$\partial((U \times V) \times V) = 3$</span>.</p>
<p>I'd like to ask how to interpret the degree of a redex and a term and if the degree values I wrote down are correct.</p>

CC BY-SA 4.0
2022-10-26T18:31:44.920Z
I assume you're taking $U, V$ atomic?
cody
CC BY-SA 4.0
2022-10-26T19:05:15.563Z
@cody Yes $U$, $V$ are atomic
Sam Ezeh
<type-theory><lambda-calculus><typed-lambda-calculus>
Interpretation of the degree of a redex
Sam Ezeh
# Interpretation of the degree of a redex

(Asked by: username_0 on 2022-10-23)

In Girard *Proofs and Types*, The degree of a type is defined as follows

$$\begin{align\*}\partial(T\_i)&=1\text{ if }T\_i\text{ is atomic}\\\partial(U\times V)=\partial(U\rightarrow V) &=\max(\partial(U), \partial(V))+1\end{align\*}$$

I interpret this as corresponding to one more than the length of the longest path in a directed graph.

[![enter image description here](https://i.sstatic.net/34A7b.png)](https://i.sstatic.net/34A7b.png)

It defines the degree of a redex as $$\begin{align\*}\partial(\pi^1\left)=\partial(\pi^2\left)&=\partial(U\times V) \text{ where }U\times V\text{ is the type of }\left\\\partial((\lambda x. v)u)&=\partial(U\rightarrow V)\text{ where }U\rightarrow V\text{ is the type of }(\lambda x. v)\end{align\*}$$ where $\pi^1$ and $\pi^2$ refer to the first and second projections of a pair with $\pi^1 \left \rightsquigarrow u$ and $\pi^2 \left \rightsquigarrow v$

It then continues to say

> The degree $d(t)$ of a term is the sup of the degrees of the redexes it contains. By convention, a normal term (i.e. one containing no redex) has degree 0.
>
> NB: A redex $r$ has two degrees: one as a redex, another as a term, for the redex may contain others; the second degree is greater than or equal to the first: $\partial(r)\leq d(r)$

I'm not sure how to interpret the definitions for the degrees of terms and redexes.

From my current understanding, if $u$ is a term of type $U$ and $v$ is a term with type $V$ then $\partial(\pi^1\left)=2$ and $\partial(\pi^1\left<\pi^1\left, \pi^2\left\right>)=2$ as the type of $\left<\pi^1\left, \pi^2\left\right>$ is again $U \times V$ and $d(\pi^1\left<\pi^1\left, \pi^2\left\right>)=2$ as all the redexes have degree 2.

For the same reason, I also think $\partial(\pi^1\left<\pi^1\left<\pi^1\left, \pi^2\left\right>, \pi^2\left<\pi^1\left, \pi^2\left\right>\right>)=2$ but $\partial(\pi^1\left<\left, v\right>)=3$ as $\partial((U \times V) \times V) = 3$.

I'd like to ask how to interpret the degree of a redex and a term and if the degree values I wrote down are correct.

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

> **Comments:**
> **username_1**: I assume you're taking $U, V$ atomic?  
> **username_0**: @username_1 Yes $U$, $V$ are atomic  

---

## 0 answers

