1 Infinitary Lambda Terms↩︎

We extend the infinitary \(\lambda\)-calculus \(\Lambda^\infty\) [1], [2] of Kennaway et alii, by adding the constant \(0\) and the function symbols \({\tt succ}\) and \({\tt cond}\). Then we define the subset \({ {\sf GTC} -\Lambda^{\infty}_T }\) of terms satisfying the Global Trace Condition (GTC), and for them we prove that all reductions are strongly convergent and all terms are total. \({ {\sf GTC} -\Lambda^{\infty}_T }\) is an extension with variables and \(\lambda\) of CT, Cyclic System \(T\) of Das [3], [4].

Our definition of \({ {\sf GTC} -\Lambda^{\infty}_T }\) is by consecutive restrictions. We first define the set \({ {\sf Row} -\Lambda^{\infty}_T }\) of infinitary row-terms with \(\lambda\) and conditional, most of which are meaningless, for which neither \(\alpha\)-renaming nor substitution is sound. Then we define the subset \({ {\sf FinVar} -\Lambda^{\infty}_T }\) of row-terms with finitely many free variables, for which we can consistently define \(\alpha\)-renaming and substitution. Then we define the subset \({\sf WTyped}\) of infinitary terms with finitely many variables that are well-typed. Eventually, we restrict well-typed infinitary terms by adding GTC, a sufficient condition for totality.

As usual, we omit unnecessary braces, assuming that \(\to\) associates to the right and term application associates to the left. We abbreviate by \(A_1, \ldots , A_n \to B\), and by \(\vec{A} \to B\) when the \(A_i\) are understood, the type \((A_1 \to \cdots (A_n \to B)\cdots)\), and say that the \(A_i\) are in argument position.

\({\sf Type}\) is the set of simple types generated by the single atomic type \(N\), whose intended interpretation is the set of natural numbers. Row-terms are possibly infinite terms representing elements of the metric completion of finite ones, namely those with a finite syntactic tree. Unlike [1] and following [5], we consider the subset \({ {\sf FinVar} -\Lambda^{\infty}_T }\) of raw terms with finite \({{\rm FV}}(t)\), the set of free variables occurring in \(t\), which admits the obvious corecursive definition. We also adapt the slightly different metric from [5] to account for truncation.

The choice of \({ {\sf FinVar} -\Lambda^{\infty}_T }\) makes it easier and unproblematic to define \(\alpha\)-equivalence and substitution, which are as follows.

In view of the above, we consider the terms in \({ {\sf FinVar} -\Lambda^{\infty}_T }\) up to \(\alpha\)-equivalence, and define substitution corecursively as follows.

In the clause [case:abs] above, the required \(z\) always exists because \({{\rm FV}}(t) \cup {{\rm FV}}(s)\) is finite, and its choice is immaterial by \(\alpha\)-equivalence.

Finally, a row term is regular if its syntactic tree is regular. We call \({ {\sf Reg} -\Lambda^{\infty}_T }\) the set of regular terms, which is clearly a (proper) subset of \({ {\sf FinVar} -\Lambda^{\infty}_T }\).

Reduction rules for \({ {\sf FinVar} -\Lambda^{\infty}_T }\), also called notions of reduction in the literature, include the usual \(\beta\)-reduction and an additional rule for the conditional.

As usual, the relation \(\mathbin{\mapsto}\) is the compatible closure of \(\mathbin{\mapsto} _\beta \, \cup \, \mathbin{\mapsto} _ {\tt cond}\), and \(\mathbin{\mapsto} ^*\) is its reflexive and transitive closure.

2 Well-typed terms and Global Trace Condition↩︎

To rule out meaningless row-terms like \(0\,0\) or \({\tt succ} (\lambda x{:}N.x)\), we introduce the typing system in Figure 1 for terms in \({ {\sf FinVar} -\Lambda^{\infty}_T }\). There are differences between our system and the inference rules of the simply typed \(\lambda\)-calculus and Gödel System \(T\). In our system, contexts are sequences of variable typings rather than sets. By \(x:A \in \Gamma\), we mean that \(x:A\) occurs in \(\Gamma\), and \(\Gamma \subseteq \Gamma'\) means that there is an injection from the first sequence into the second, possibly including permutations. We explicitly list the rule \({\tt wk}\) for weakening+exchange, which is not merely admissible. Further, the application rule is split into the rules \({{\tt ap}_{\tiny v}}\) and \({\tt ap} _{\neg v}\), depending on whether the term \(s\) in the subject \(t\,s\) of the conclusion is a variable: \({{\tt ap}_{\tiny v}}\) corresponds to a contraction between two occurrences of \(A\) in Logic. Finally, we add a pair of relations, represented by and arrows, linking variables in type contexts and types in the argument position of the derived type in the conclusion to variables and types in the premises of each rule. These relations are essential to the definition of traces below.

We observe that both terms and derivations may be infinite trees, and only finite terms in \({\sf WTyped}\) are typable by finite derivations. A well-typed term does not necessarily have a unique derivation and type, even when the type context is fixed. Consider the family of closed terms \(t_n = t_{n+1} \,0\); then for each \(n \in \mathbb{N}\) we can find a derivation of \(\vdash t_n :N^n \rightarrow A\), where \(N^n\) is a list of \(n\) occurrences of \(N\) and \(A\) is arbitrary. Moreover, derivations are too weak to filter out infinite terms of the form \(t = (\lambda x{:}N.t)\,0: A\) or \(t = {\tt cond} (t, \lambda x{:}N.t)\, {\tt succ} (0): A\) that reduce infinitely often to a redex, never returning a meaningful output. These terms are called active in Kennaway et alii [1], [2]. We introduce the Global Trace Condition (GTC) for our system by adapting concepts from [4], [6] that rule out active well-typed terms. Moreover, the condition GTC rules out closed terms of type \(N\) that do not denote numbers, such as \(t = {\tt succ} (t) : N\), or do not denote total functionals, and enforces the uniqueness of typing.

In Figure 2, we illustrate the proof of the typing of the term \({\tt sum} = \lambda x{:}{N}. {\tt cond} (x,\lambda y{:}{N}. {\tt succ} ( {\tt sum} \,x\,y))\) for summation. We depict only the relevant arrows of the trace relations. Since \({\tt sum} \in { {\sf Reg} -\Lambda^{\infty}_T }\) (namely, it is regular), the proof itself is regular, and we represent it by a finite cyclic graph, where the only cycle is represented by the pair of the two \((\dagger)\) connected by a black arrow.

The proof of \(\Gamma \vdash t:A\) claimed in Theorem [theorem-uniqueness-typing] is not unique in general. However, it can be transformed into a (unique) canonical form by: (i) restricting the conclusion \(\Gamma' \vdash u:B\) of each instance of rule \(\not = {\tt wk}\) so that \({{\rm dom}}(\Gamma') = {{\rm FV}}(u)\); (ii) collapsing any two consecutive \({\tt wk}\) into one; (iii) removing identical \({\tt wk}\) and possibly adding at most one \({\tt wk}\) to the end.

Intuitively, a progress point represents the application of the conditional \({\tt cond} (t, s)\) to decreasing values of its argument. All other references to argument terms or potential values of free variables are considered stationary, meaning their values in an actual computation need not decrease. The GTC prevents infinite computations involving infinitely decreasing values of type \(N\). This is stated in the next section, where we relate infinitely progressing traces to strongly convergent reductions of transfinite length.

3 Infinite reduction and strong convergence↩︎

Given an ordinal \(\alpha\), either finite or infinite, a sequence of terms \((t_\beta)_{\beta < \alpha}\) is a reduction of length \(\alpha\) if for all \(\beta < \alpha\) we have \(t_\beta \mathbin{\mapsto} t_{\beta + 1}\). In the theory of the infinitary \(\lambda\)-calculus, normal forms (terms not including any redex) might be reached only in the limit, after infinitely many reduction steps; consistently, the concept of normalizing reduction is replaced by that of strongly convergent reduction, which does not necessarily yield a normal form but rather generates a sequence of terms that is Cauchy-convergent with respect to the term distance and such that the depth of contracted redexes tends to infinity (see [2]).

To reconcile strong convergence with the idea of strong normalization in type theory, we consider a stronger notion of possibly infinite reduction, which we call \({\tt cond}\)-convergence. In the following, a position is a finite string \(p \in \{ 1,2 \}^*\) representing a node in the syntactic tree of a term \(t \in { {\sf FinVar} -\Lambda^{\infty}_T }\), where the empty sequence is the root of \(t\); if \(t = \lambda x{:}A.t'\) or \(t = {\tt succ} (t')\) and \(p = 1\,q\), then \(p\) is the position \(q\) in \(t'\); if \(t = t't''\) or \(t = {\tt cond} (t',t'')\), then \(p = 1\,q\) is the position \(q\) in \(t'\), and \(p = 2\,q\) is the position \(q\) in \(t''\). If \(p\) is a position in \(t\), then \(t \upharpoonright p\) denotes the subterm of \(t\) rooted at \(p\).

In words, a position \(p\) of a term \(t\) encodes a finite path from the root of the syntactic tree of \(t\); it has \({\tt cond}\)-depth \(n\) if it passes through the tree of the subterm \(t_2\) of some occurrence of \({\tt cond} (t_1, t_2)\) in \(t\) exactly \(n\) times. Remember that \({\tt cond} (t_1,t_2)( {\tt succ} (u)) \mathbin{\mapsto} t_2 (u)\), thereby mimicking the recursion mechanism via the nesting of \({\tt cond}\) in \(t_2\). Hence, an infinite \({\tt cond}\)-convergent reduction is one in which no redex on the right branch of a \({\tt cond}\) can be contracted infinitely often.

Any \({\tt cond}\)-convergent reduction is strongly convergent, but not vice versa. We can establish the following results.

We briefly mention additional properties of terms in \({ {\sf GTC} -\Lambda^{\infty}_T }\) that are not covered in the paper. Typability is preserved not only under finite reductions, as stated in Theorem 1.[thr:SR], but also in the limit. As for \(\Lambda^\infty\), confluence does not hold in general because of infinite reductions, but it holds in the limit. This allows us to show that the numeral in [thr:main-3] above is unique. Finally, we conjecture that the expressive power of our system is the same as that of Das’s system \(CT\) and, hence, Goedel’s system \(T\).

References↩︎