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

It defines the degree of a redex as $$\begin{align*}\partial(\pi^1\left<u, v\right>)=\partial(\pi^2\left<u, v\right>)&=\partial(U\times V) \text{ where }U\times V\text{ is the type of }\left<u, v\right>\\\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<u, v\right> \rightsquigarrow u$ and $\pi^2 \left<u, v\right> \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<u, v\right>)=2$ and $\partial(\pi^1\left<\pi^1\left<u, v\right>, \pi^2\left<u, v\right>\right>)=2$ as the type of $\left<\pi^1\left<u, v\right>, \pi^2\left<u, v\right>\right>$ is again $U \times V$ and $d(\pi^1\left<\pi^1\left<u, v\right>, \pi^2\left<u, v\right>\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<u, v\right>, \pi^2\left<u, v\right>\right>, \pi^2\left<\pi^1\left<u, v\right>, \pi^2\left<u, v\right>\right>\right>)=2$ but $\partial(\pi^1\left<\left<u, v\right>, 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.

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.