# Interpretation of the degree of a redex

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

• I assume you're taking $U, V$ atomic?
– cody
Oct 26, 2022 at 18:31
• @cody Yes $U$, $V$ are atomic Oct 26, 2022 at 19:05