patternMinor
Definition of a size of type
Viewed 0 times
definitionsizetype
Problem
In B. Pierce's book "Types and Programming Languages", he talks about the size of types (see pictures below).
I searched the book for a definition but could not find one. I only found a definition for the size of terms, but not for the size of types.
Could someone please explain what Pierce means by the expression "$size(T_1)$" (marked by yellow in the image below) ?
I searched the book for a definition but could not find one. I only found a definition for the size of terms, but not for the size of types.
Could someone please explain what Pierce means by the expression "$size(T_1)$" (marked by yellow in the image below) ?
Solution
A term in logic and rewriting theory is anything defined by a tree structure that's supposed to represent the syntax of something. It can be a term of a programming language, a type, a kind, a module, etc.
The size of a term is the size of the tree: it's 1 for a leaf, and $\mathit{size}(t) = \mathit{size}(t_1) + \dots + \mathit{size}(t_n)$ for a tree $t = C(t_1,\dots,t_n)$. The exact definition is often not terribly important: what matters is that the size of a term is strictly larger than the size of any term that appears as a part of it.
In programming language literature, some authors use term in this sense, and some authors use term for a term of the programming language itself as opposed to types, kinds, modules, etc. The former authors use expression for the narrow sense of a term of the programming language itself. Pierce uses term in the narrow sense.
The definition of the size follows the same principle no matter what syntactic category the term (in the broader sense) represents. Thus the size of a type is defined as $\mathit{size}(\mathsf{Nat}) = \mathit{size}(\mathsf{Bool}) = 1$, $\mathit{size}(\mathsf{T}_1 \mathord\rightarrow \mathsf{T}_2) = 1 + \mathit{size}(\mathsf{T}_1) + \mathit{size}(\mathsf{T}_2)$, etc.
When there are multiple syntactic categories, whether terms of another category count depends on the definition chosen by the author. For example, the size of $\lambda x:T. M$ could be defined as $1 + \mathit{size}(M)$, or as $1 + \mathit{size}(T) + \mathit{size}(M)$, or even as $1 + \mathit{size}(x) + \mathit{size}(T) + \mathit{size}(M)$ depending on what is convenient for the matters at hand.
The size of a term is the size of the tree: it's 1 for a leaf, and $\mathit{size}(t) = \mathit{size}(t_1) + \dots + \mathit{size}(t_n)$ for a tree $t = C(t_1,\dots,t_n)$. The exact definition is often not terribly important: what matters is that the size of a term is strictly larger than the size of any term that appears as a part of it.
In programming language literature, some authors use term in this sense, and some authors use term for a term of the programming language itself as opposed to types, kinds, modules, etc. The former authors use expression for the narrow sense of a term of the programming language itself. Pierce uses term in the narrow sense.
The definition of the size follows the same principle no matter what syntactic category the term (in the broader sense) represents. Thus the size of a type is defined as $\mathit{size}(\mathsf{Nat}) = \mathit{size}(\mathsf{Bool}) = 1$, $\mathit{size}(\mathsf{T}_1 \mathord\rightarrow \mathsf{T}_2) = 1 + \mathit{size}(\mathsf{T}_1) + \mathit{size}(\mathsf{T}_2)$, etc.
When there are multiple syntactic categories, whether terms of another category count depends on the definition chosen by the author. For example, the size of $\lambda x:T. M$ could be defined as $1 + \mathit{size}(M)$, or as $1 + \mathit{size}(T) + \mathit{size}(M)$, or even as $1 + \mathit{size}(x) + \mathit{size}(T) + \mathit{size}(M)$ depending on what is convenient for the matters at hand.
Context
StackExchange Computer Science Q#35291, answer score: 5
Revisions (0)
No revisions yet.