Intersection Types for Unboundedness Problems
Pawe{\l} Parys (Institute of Informatics, University of Warsaw)
TL;DR
This paper surveys how intersection types can be used to analyze and estimate quantitative properties of simply typed lambda-terms, focusing on unboundedness problems.
Contribution
It introduces two type systems that estimate the frequency and maximal occurrences of constants in lambda-terms' normal forms.
Findings
First type system estimates total appearances of a constant.
Second type system estimates maximum appearances on a branch.
Provides tools for analyzing unboundedness in lambda calculus.
Abstract
Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter option; more precisely, on the use of intersection types for describing quantitative properties of simply typed lambda-terms. We present two type systems. The first allows to estimate (by appropriately defined value of a derivation) the number of appearances of a fixed constant 'a' in the beta-normal form of a considered lambda-term. The second type system is more complicated, and allows to estimate the maximal number of appearances of the constant 'a' on a single branch.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Intersection Types for Unboundedness Problems††thanks: Work supported by the National Science Centre, Poland (grant no. 2016/22/E/ST6/00041).
Paweł Parys Institute of Informatics, University of Warsaw, Poland [email protected]
Abstract
Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter option; more precisely, on the use of intersection types for describing quantitative properties of simply typed lambda-terms. We present two type systems. The first allows to estimate (by appropriately defined value of a derivation) the number of appearances of a fixed constant in the beta-normal form of a considered lambda-term. The second type system is more complicated, and allows to estimate the maximal number of appearances of the constant on a single branch.
1 Introduction
Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter option; more precisely, on the use of intersection types for describing quantitative properties of simply typed lambda-terms.
We consider lambda-terms as generators of trees. To this end, we assume a unique ground sort111Following the convention in this area, we use the word “sort” for simple types, and the word “type” for intersection types refining them. describing trees, and we assume some uninterpreted constants, which are functions of order at most . Then, a beta-normal form of a closed lambda-term of the ground sort does not contain any lambda-binders—it is just an applicative term composed of the uninterpreted constants, and thus can be seen as a tree. In other words, in the effect of calling a function with some trees as arguments, we obtain a new tree with a root labeled by , and with the arguments attached in the children of the root.
Suppose now that we have a closed lambda-term of the ground sort, and we want to estimate some quantities concerning its beta-normal form . As a first example of such a quantity we can take the number of appearances of some fixed constant in . How can we read this number from the original lambda-term ? As a first approach, we can look at the number of appearances of the constant in . This can be completely inappropriate, though, for two reasons. First, we can have in some appearances of the constant that will be removed during beta-reductions. Second, maybe the constant appears in only once, but it will be replicated a lot of times during beta-reductions. In order to take into account these two phenomena we design an appropriate type system; a type derivation for the lambda-term identifies the places in that are really responsible for producing some constants in the beta-normal form , so that these places can be counted. The type system realizing this goal is presented in Section 3.
Another quantity of the tree is the largest number of appearances of some fixed constant on a single branch in . While the quantity of the first kind can be called deterministic, this one is slightly more complicated, and can be called nondeterministic. The justification of such a name is that while looking locally at some fragment of we do not know whether the constants appearing in this fragment should be counted or not (i.e., whether they are located on the branch of containing the largest number of constants ). We thus have to non-locally (nondeterministically) choose some branch of on which the constants should be counted. A type system that allows to estimate the above quantity is presented in Section 4.
The following quantity is even more involved: what is the largest number such that the binary tree with all nodes labeled by and all branches of length embeds homeomorphically in the considered tree ? In a sense, this quantity combines three elements: taking the maximum, taking the minimum, and counting. Indeed, we take here the maximum over all embeddings of trees with all nodes labeled by of the minimum of lengths of paths in the chosen tree (and internally, we count the number of constants on the chosen path). Unfortunately, the presented methods do not allow to estimate this quantity; it is an open problem to construct a type system concerning this quantity.
One may wonder why we want to have the aforementioned type systems, instead of just expanding the lambda-term into its beta-normal form , and computing the quantity there. The answer is: compositionality. Suppose that is an application . If we know types derivable for and for , we can determine types derivable for . Moreover, knowing the quantities assigned to type derivations for and for we can determine the quantity assigned to type derivations for . We thus have a composable abstraction of every lambda-term: a set of its types, and a tuple of numbers (with a bound on the size of this set and on the length of this tuple that depends only on the sort of the lambda-term, not on its size). Existence of such an abstraction has some interesting implications.
In particular, the research presented here is motivated by applications in the area of higher-order recursion schemes. Recursion schemes, or equivalently terms of the -calculus, form an extension of the simply typed lambda-calculus by a fixed-point operator [12, 18, 23, 22]. Trees generated by recursion schemes can be used to faithfully represent the control flow of programs in languages with higher-order functions [19]. We remark that the same class of trees can be generated by collapsible pushdown systems [16] and ordered tree-pushdown systems [8].
Intersection type systems were intensively used in the context of recursion schemes, for several purposes like model-checking [19, 22, 6, 30], pumping [20, 3], transformations of HORSes [21, 2, 9], etc. Interestingly, constructions very similar to intersection types were used also on the side of collapsible pushdown systems; they were alternating stack automata [5], and types of stacks [24, 17]. The type systems are also closely connected to linear logic [15, 14].
The type system of Section 3 is based on the type system from Parys [25]. A similar type system was used to prove that some trees generated by recursion schemes cannot be generated by so-called safe recursion schemes [24]. The type system of Section 4 comes from Parys [26, 27]. It implies decidability of the model-checking problem for trees generated by recursion schemes against formulae of the WMSO+U logic [29]. It also allows to solve the simultaneous unboundedness problem (aka. diagonal problem) for recursion schemes, which was first solved in a different way [9].
2 Preliminaries
The set of sorts is constructed from a unique basic sort using a binary operation . Thus is a sort and if are sorts, so is . The order of a sort is defined by: , and ; in other words, whenever .
A signature is a set of constants, that is, symbols with associated sorts. For simplicity, in this paper we use a signature consisting of three constants: of sort , and of sort , and of sort (it is easy to generalize the methods to an arbitrary signature, assuming that sorts of constants are of order at most ).
The set of (simply typed) lambda-terms is defined by induction as follows:
- •
constants (node constructors)—a constant of sort is a lambda-term of sort ;
- •
variables—for each sort there is a countable set of variables that are also lambda-terms of sort ;
- •
lambda-binders—if is a lambda-term of sort and a variable of sort then is a lambda-term of sort ;
- •
applications—if is a lambda-term of sort and is a lambda-term of sort then is a lambda-term of sort .
As usual, we identify lambda-terms up to alpha-conversion (renaming of bound variables). We often omit the sort annotation of variables, but please keep in mind that every variable is implicitly sorted. A term is called closed when it does not have free variables. The order of a lambda-term , denoted , is defined as the order of the sort of , while the complexity of is defined as the maximum of orders of subterms of .
A sort is homogeneous if and all are homogeneous (defined by induction). A lambda-term is homogeneous if all its subterms have homogeneous sorts. In order to avoid some technicalities, in this paper we only consider homogeneous lambda-terms. This is without loss of generality, since there is a simple syntactic transformation converting every closed lambda-term of sort into a homogeneous lambda-term having the same beta-normal form [28].
We use the usual notion of beta-reduction: we have if can be obtained from by replacing some of its subterms of the form by . We recall that simply typed lambda-calculus has the properties of strong normalization and confluence, that is, every sequence of beta-reductions from a lambda-term eventually terminates in a unique lambda-term such that no more beta-reductions can be performed from ; the lambda-term is called the beta-normal form of . Observe that the beta-normal form of a closed lambda-term of sort is an applicative term build of constants (it does not contain variables nor lambda-binders), and thus can be seen as a tree (generated by the lambda-term).
In this paper we are interested in two particular reduction strategies (i.e., strategies of choosing a redex that should be reduced next). In the OI strategy, we always reduce an outermost redex, that is, a redex that is not located inside another redex. Notice that if is closed and of sort , then every outermost redex in is also closed. A redex is a redex of order if . Assuming that the lambda-term is homogeneous, we have if and only if . In the RMF strategy we always reduce a rightmost redex of the maximal order, that is, a redex of some order such that in the lambda-term there is no redex of a higher order, and in there are no redexes of order , and the redex is not located inside for some order- redex . In other words, whenever we see an order- redex , we first reduce all order- redexes in , then the redex itself, and then we continue reducing the resulting lambda-term. We also write RMF to make it explicit that the order of the considered redex is . When a closed lambda-term of sort has complexity (and is not in the beta-normal form), then an RMF reduction always exist; thus following the RMF strategy we first reduce all redexes of order (until reaching a term of complexity ), then all redexes of order , and so on. Moreover, for an RMF redex in such a lambda-term, all variables appearing in are of order at most .
Suppose that we have two functions , over some domain . We want to define when estimates . To this end, we say that is dominated by , written , if there exists a function such that for all , and we say that estimates , written , if and . It is easy to see that estimates if and only if on every subset of the domain , the functions and are either both bounded or both unbounded. The above relation between functions is widely used in the area of regular cost functions (see, e.g., Colcombet [10]).
One may also consider infinite lambda-terms. Clearly they do not reduce to a normal form in a finite number of steps, but we can consider the (unique) normal form reached in the limit, called the Böhm tree. As in the finite case, the Böhm tree of a closed lambda-term of sort is a (potentially infinite) tree build out of constants. A recursion scheme is a finite description of a regular (i.e., having finitely many different subterms) infinite lambda-term.
3 Deterministic Quantities
In this section we present a type system that allows to estimate the number of appearances of the constant in the beta-normal form of a lambda-term. The type system should be such that a type derivation for a closed lambda-term of sort identifies the places in that are responsible for producing some -labeled nodes in the beta-normal form of . To this end, we extend the notion of sorts by a productivity flag, which can be (standing for productive) and (standing for nonproductive).
It may happen that a single lambda-term has multiple types; for example, is productive when the function (substituted for) uses its argument, and nonproductive otherwise. Because of that, we need intersection types (i.e., the ability of assigning multiple types to the same lambda-term).
In effect, our types differ from sorts in that on the left side of , instead of a single type, we have a set of pairs , where is a type, and is a flag from . The unique atomic type is denoted . More precisely, for each sort we define the set of types of sort as follows:
[TABLE]
where denotes the powerset. A type is denoted as , or when . The empty intersection is denoted by . To a lambda-term of sort we assign not only a type , but also a flag (which together form a pair ).
Intuitively, a lambda-term has type when it can return , while taking an argument for which we can derive all pairs (of a flag and a type) from ; simultaneously, while having such a type, the lambda-term is obligated to use its arguments in all ways described by type pairs from . And, we assign the flag (productive), when this term (while being a subterm of a closed term of sort ) increases the number of constants in the resulting tree. To be more precise, a term is productive in two cases. First, when it uses the constant . Notice however that this has to be really used: there exist terms which syntactically contain , but the result of this is then ignored, like in . Second, a term which takes a productive argument and uses it at least twice is also productive (for example, the productive argument may be a function that creates an -labeled node; when a lambda-term uses such an argument twice, the lambda-term is itself responsible for increasing the number of constants in the resulting tree).
A type judgment is of the form , where we require that the type and the term are of the same sort. The type environment is a set of bindings of variables of the form , where . In we may have multiple bindings for the same variable. By we denote the set of variables that are bound by , and by we denote the set of those binding from that use flag .
We now gradually present rules of the type system. We begin with rules for node constructors:
[TABLE]
Since we aim at counting constants , we say here that is productive, while and are nonproductive. Notice that productivity of a node constructor does not depend on productivity of the argument; flags of the arguments () can be arbitrary.
Then we have a rule for a variable:
[TABLE]
The type of the variable is taken from the environment. The flag is always , though; by just using a variable we are not productive at all (and in the productivity flag we want to cover productivity of the lambda-term itself, not of lambda-terms that may be potentially substituted for free variables).
The rule that talks about lambda-binders is very natural; it just moves type pairs from the argument to the environment:
[TABLE]
Finally, we have the most complicated rule, for application:
[TABLE]
where we assume that
- •
every pair is different (where ),
- •
for each , if and only if or , and
- •
if and only if , or for some , or .
Let us explain the above conditions. The first condition is technical: we need to provide exactly one derivation for every needed type pair. The second condition says that when requires a “productive” argument, either we can apply an argument that is itself productive, or we can apply a nonproductive that uses a productive variable; in the latter case, after substituting something for the variable, will become productive. The third condition says that is productive if is productive, or if is productive, or if some productive free variable is duplicated (i.e., used in at least two subderivations simultaneously).
Notice that weakening of type environments is disallowed: does not necessarily imply ; in other words, every binding in the type environment (and thus every pair assigned to an argument) has to be really used somewhere in the type derivation. This property of the type system is very expected, if we recall that we want to distinguish lambda-terms that really use their (productive) arguments from those in which the arguments are discarded. On the other hand, contraction is allowed: we may say that implies , since a type environment is a set of type bindings. As we see in the (@) rule, such contractions (for productive type binding) cause productivity of lambda-terms.
A derivation is defined as usual: it is a tree labeled by type judgments, such that each node together with its children fit to one of the rules of the type system.
We now define a value of every node of a derivation, saying how much this node is productive. In a node using the rule for the constant , the value is . In a node using the (@) rule with type environments and for , the value is
[TABLE]
Spelling this out, the value in such a node equals the number of productive type bindings together in all the type environments , , minus the number of such type bindings in their union. In other words, it says how many times we have to duplicate some productive type bindings before splitting them between type environments of subderivations. In all other nodes the value is [math].
For a derivation , the value of , denoted , is the sum of values of all nodes in . We can easily see that the value of a derivation is positive if and only if is productive (i.e., the flag in the derived type judgment is ). The main theorem says that can be used to estimate the the number of constants in normal forms of lambda-terms.
Theorem 1**.**
The following holds for the type system introduced above:
- (D1)
for every there is a function such that if is a homogeneous and closed lambda-term of sort and complexity at most , and is a derivation for , then the number of constants in the normal form of is
- (D1A)
at least , and 2. (D1B)
at most ; 2. (D2)
for every closed lambda-term of sort one can derive (for some ).222Actually, one can even prove that there is a unique derivation concerning (assuming that is closed and of sort ).
Example 1**.**
Observe how the type system behaves for the lambda-term , where . We start with a derivation concerning , where we write for :
[TABLE]
Notice that the type requires a productive argument, but (in both the (@) rules above) we apply an argument that is not productive itself. This is possible, because the type judgments for the arguments have productive type bindings in the type environments (and hence for the purposes of the (@) rule they are assumed to be productive). The lower use of the (@) rule has value (and in effect the productivity flag is set to ), because the productive type binding is taken to both children.
Below, we have another derivation concerning , where we write for :
[TABLE]
This time the value of all nodes is [math], because every type binding is used in exactly one place. Likewise, it is possible to derive five other type pairs for the lambda-term :
[TABLE]
While deriving a type for , we only need one type pair for : the type pair derived at the beginning. But we remark that if the lambda-term was (we have replaced here by , and thus the first call to receives a nonproductive argument as ), it would be necessary to use both the above derivations for .
Denoting the type as , we continue the derivation for :
[TABLE]
The total value of this derivation is ( in the two nodes concerning , and in the three subderivations concerning ), while the normal form of contains appearances of the constant . Notice that while adding any further to the sequence , we increase the value by , while we almost double the number of ’s in the normal form.
Proofs.
Let us now sketch the proof of Theorem 1. While proving Condition (D1), it is convenient to consider the RMF strategy of reductions (defined on Page 2). We have the following subject-reduction lemma for reductions of this kind.
Lemma 2**.**
If is a derivation for , where is homogeneous, closed, and of complexity (and of sort ), and is a sequence of RMF beta-reductions, then there exists a derivation for such that and .
Because the maximal complexity of the lambda-term considered in Theorem 1 is fixed, using Lemma 2 times (for complexities ) we obtain a derivation for the normal from of such that and is bounded by a function of , that is, estimates . It remains to notice that is exactly the number of -labeled nodes in the tree .
Proof sketch (Lemma 2).
We proceed by induction: for every out of the derivation for we construct a derivation for . To this end, we consider every subderivation of starting with a type judgment concerning the redex involved in the reduction ; we need to replace it by a derivation for . We obtain by a surgery on : we take the subderivation of concerning , we replace every leaf deriving a type for by the subderivation of deriving this type for , and we update type environments and productivity flags appropriately.
Notice that every subderivation concerning is moved to at least one leaf concerning (nothing can disappear). The only reason why the value of the derivation can decrease is that potentially a productive type binding was duplicated (say, times) in the derivation concerning . In this binding is no longer present (in there is no ) so the value gets decreased by , but in this situation the subderivation deriving for becomes inserted in leaves. This subderivation is either productive itself, or uses a productive type binding in the environment; in both cases by creating additional copies of this subderivation we increase the value at least by , compensating the loss caused by elimination of . This implies that , hence (and, in effect, ).
Conversely, the only reason why the value can grow is that some derivation concerning (that is either productive itself or uses some productive type bindings for its free variables) becomes inserted in leaves, for some . In the worst case, this may cause that the value (of the whole derivation for ) gets multiplied by . But, simultaneously, in the subderivation concerning , the productive type bindings for are removed, which decreases the value by in some nodes of this subderivation. The point is now that these nodes were never copied in the reduction sequence from to the considered ; this is because all the reductions are RMF reductions. Indeed, looking from the other side, all variables appearing in (the copied subderivation for) are of order at most —as observed on Page 2—but all variables involved in future order- reductions (i.e., all variables that we remove from type environments) are of order —because of homogeneity of the lambda-term. Thus, whenever we multiply the value of the current derivation by at most , we subtract from the value of the original derivation . The worst case is when times we decrease the value by , and times we multiply it by . It follows that ; a slightly more careful analysis shows that actually . ∎
In the proof of Condition (D2), saying that we can derive a type for every closed lambda-term of sort , we proceed backwards: it is easy to derive a type for a tree (i.e., for the normal form of ), and thus it is enough to have a subject expansion lemma saying that out of a derivation for a lambda-term after a beta-reduction we can construct a derivation for the lambda-term before the beta-reduction. This time we follow the OI reduction strategy. Because outermost redexes are closed, it is thus enough to have the following lemma.
Lemma 3**.**
If we can derive , then we can also derive .
Proof sketch.
In the derivation for we replace every subderivation concerning by a leaf rule for the variable , and we correct type environments and productivity flags in the rest of the derivation. This way we obtain a derivation for with type environment requesting some types for . Simultaneously, each of these types was derived for in some subderivation of (there may be multiple such subderivations, because may appear in many places in , but we choose only one subderivation for every type). It is not difficult to combine these derivations into a derivation concerning . ∎
We remark that by applying the above surgery to a derivation for (i.e., for an arbitrary redex, having some free variables) we only obtain a derivation for with some , but not necessarily with . The reason is that we remove some subderivations concerning (we leave only one for every type), and possibly some type bindings from were used only in the removed subderivations.
Bibliographic Note.
As already mentioned in the introduction, the idea of the type system presented above originates from Parys [24]. In that paper, a similar type system was introduced for configurations of collapsible pushdown systems. It was then used to prove that a restricted variant of these systems (systems without the so-called collapse operation) are less powerful than general collapsible pushdown systems. The type system was then transferred to the setting of lambda-terms in Parys [25]. Their type system is slightly more complicated than ours, and allows to obtain a stronger version of Condition (D1B), where the function does not depend on the complexity of considered lambda-terms.
4 Nondeterministic Quantities
Suppose now that we want to estimate another quantity: the maximal number of appearances of the constant on a single branch in the beta-normal form of a lambda-term . It seems that in order to describe this quantity, it is enough to take the type system from Section 3, and replace the rule for the constant by two rules:
[TABLE]
In these rules we ignore one of the arguments, and we descend only to the other one. This way, every type derivation for a tree follows one branch in , and in effect equals to the number of constants on that branch. By arguments like in the previous section we obtain the following, rather useless, properties of the modified type system:
- (N1)
for every there is a function such that if is a homogeneous and closed lambda-term of sort and complexity at most , and is a derivation for , then the number of constants on some branch of the normal form of is
- (N1A)
at least , and 2. (N1B)
at most ; 2. (N2)
for every closed lambda-term of sort one can derive (for some ).
These properties are not satisfactory for us, because they only say that there exists a branch with the number of constants estimated by , for some derivation . We, however, are interested in the branch on which the number of constants is maximal. In other words: if in the beta-normal form of there are two branches, one with just a few constants , and the other with a lot of them, we expect to have two derivations and , where is small (corresponds to the first branch), and is large (corresponds to the second branch). But Condition (N2) gives us only one derivation, and we do not know which one. Thus, we rather need to have the following property:
- (N2*′*)
for every there is a function such that if is a homogeneous and closed lambda-term of sort and complexity at most and on some branch of the beta-normal form of there are appearances of the constant , then there is a derivation for such that .
In the light of Condition (N2*′*), Condition (N1B) becomes redundant, and thus we can restate Condition (N1A) as follows:
- (N1*′*)
if is a homogeneous and closed lambda-term of sort , and is a derivation for , then the number of constants on some branch of the normal form of is at least .
It is, though, an open problem whether Condition (N2*′*) holds.
Open Problem 1**.**
Does the modified type system satisfy Condition (N2*′*)?
In order to prove Condition (N2*′*), we should probably proceed backward: we should start with a derivation concerning (the branch with the maximal number of constants in) the normal form of , and then, successively, from a derivation for a lambda-term after a beta-reduction obtain a derivation for the lambda-term before the beta-reduction. We have a subject expansion lemma (Lemma 3) only for redexes without free variables (and it seems difficult to generalize it to arbitrary redexes, as explained at the end of the previous section); we should thus assume that we always reduce the outermost redex. In effect, in the considered sequence of beta-reductions from to its normal form we have to mix reductions concerning redexes of different orders. For such a sequence of reductions it is not clear how to estimate the value of the derivation for the beta-normal form by the value of the derivation for .
We remark that a modified type system, in which one allow weakening of type environments, satisfies a subject expansion lemma (like Lemma 3). But with unrestricted weakening of type environments Condition (N1*′*) no longer holds. Indeed, if weakening was allowed, we could use a derivation (with an arbitrary large value) for a lambda-term as a part of a derivation for a lambda-term like , whose normal form contains no . The reason why weakening is forbidden is exactly this: we want to have subderivations only for subterms that really participate to the normal form.
The life is thus not so simple: because we want both Conditions (N1*′*) and (N2*′*), we have to introduce a more complicated type system. In this type system, instead of one kind of values of nodes, we have values of order (or -values) for every (where is the complexity of the considered lambda-term). We also mark some nodes as belonging to a zone of order (or -zone) for every order .
Before defining the type system, let us first give some idea how Condition (N2*′*) can be shown. Then, we give details of a type system motivated by this idea.
Consider thus a lambda-term that is of complexity , and reduces to a tree . Following the RMF reduction strategy, we can find lambda-terms such that every is of complexity and all reductions between and are of order . Our aim is to estimate the number of constants located on some branch in . We thus mark all nodes of this branch as the [math]-zone, and we say that the order- value is in all nodes of the [math]-zone that are labeled by . Next, we proceed back to . Every node constructor in the [math]-zone in originates from some particular node constructor appearing already in . We thus mark these node constructors in as belonging to the [math]-zone (notice that in they no longer form a branch); and again those of them that are -labeled get -value . The crucial observation is that no two node constructors from the [math]-zone in can originate from a single node constructor of . Indeed, all the beta-reductions between and are RMF. In such a beta-reduction we take a whole subtree (i.e., a lambda-term of sort ) of , and we replace it somewhere, possibly replicating it. But since the considered nodes of lie on a single branch, they may belong to at most one copy of the replicated subtree. In effect, the total -value in is the same as in .
We cannot directly repeat the same reasoning to move -values from back to , since now there is a problem: a single node constructor in may result in multiple (uncontrollably many) node constructors with a -value in . We rescue ourselves in the following way. We choose some branch of (included in the [math]-zone) as the -zone. Then, for every node of with positive -value, we look for the closest ancestor of this node that lies in the -zone, and in this ancestor we set the -value to . Notice that for multiple nodes with positive -value, their closest ancestor lying in the -zone may be the same (and then we set its -value to , not to the number of these nodes). Thus, in general, the total -value may be smaller than the total -value. We can, however, ensure that it is smaller only logarithmically; to do so, we choose a branch forming the -zone in a clever way: staring from the root, we always proceed to the subtree with the largest total -value. In effect, the total -value of estimates the total -value of .
Once all nodes of with positive -value lie on a single branch (which is chosen as the -zone), we can transfer them back to without changing their number: because reductions between and are RMF, every node of the -zone in originates from a different node of . Then in we again choose a branch as the -zone, we assign -value to some its nodes, and so on. At the end we obtain some labeling of by zones and values of particular orders. The goal of the type system presented below is, roughly speaking, to ensure that a labeling of actually is obtainable in the process as above. In fact, we do not label nodes of itself, but rather nodes of a type derivation for .
We now come to a formal definition of the type system.
Type Judgments.
For every sort we define the set of types of sort , and the set of type triples of sort . This is done as follows, where denotes the powerset:
[TABLE]
Notice that the sets and are finite. A type is denoted as . A type triple consists of a zone order , a productivity order , and a type . In order to distinguish types from type triples, the latter are denoted by letters with a hat, like .
A type judgment is of the form , where , called a type environment, is a set of bindings of the form with , and is a lambda-term, and is a type triple of the same sort as (i.e., when is of sort ). We assume that is homogeneous.
As previously, the intuitive meaning of a type is that a lambda-term having this type can return a lambda-term having type , while taking an argument for which we can derive all type triples from . Moreover, in there is just one type , which can be assigned to every lambda-term of sort . Suppose that a node of a type derivation for a closed and homogeneous lambda-term of sort is labeled by a type judgment with . Then
- •
is the type derived for ;
- •
contains type triples that could be used for free variables of in the derivation;
- •
is an upper bound for the complexity of (this bound is not strict: in the proofs, it is useful to temporarily allow also lambda-terms of complexity ), and simultaneously for orders of considered zones and values;
- •
is the largest number such that for every , the considered node of the derivation belongs to the -zone;
- •
is the largest number such that for every , in the imaginary lambda-term obtained from by reducing all redexes of order greater than , the order- value will be positive in the subderivation starting in the considered node.
Notice that we always have that , which means that every node of every derivation belongs at least to the [math]-zone. We choose zones in a derivation in such a way that for every node the set of orders of zones to which the node belongs is always of the form . For this reason in a type triple it is enough to have a number (representing the set ), instead of an arbitrary set of orders of zones. Moreover, if a node of a derivation belongs to a -zone, then its parent as well; in effect, the zone order in the type triple labeling a parent cannot be smaller than in its child. Likewise, the set of orders for which the -value is positive (after appropriate reductions) is always of the form , so it is enough to remember its maximum. Moreover, if -value is positive is some subderivation, then it is also positive in a larger subderivation, hence also the productivity order in the type triple labeling a parent cannot be smaller than in a child.
Type System.
We now give the first four rules, concerning node constructors:
[TABLE]
We say that the -value in a node using the rule for the constant is for all ; for , and for the other constants the -value is [math].
In the above rules we can choose arbitrarily (from the set ), which amounts to deciding to which zones the node constructor should belong: it belongs to the -zone for . For the constant we descend only to one argument (because we want to count constants only on a single branch of the normal form). For the constant we have set the -value to for all , hence we set the productivity order to . There is an exception for : by definition of , the productivity order can be at most , so although the -value is as well, this information is not covered by the productivity order. Notice that the type assigned to arguments of node constructors is the only element of ; node constructors do not receive information about zones or values from their arguments.
Next, we have a rule for a variable (in nodes using this rule, the -value is [math] for all ):
[TABLE]
In order to understand this rule, suppose that it labels a node of a type derivation for a closed lambda-term of sort . Take some , and consider the lambda-term obtained from our lambda-term by reducing all redexes of orders greater than . According to the proof idea presented above, we create the -zone as a branch of (and then we transfer it back to ). Moreover, as the productivity order we should take at least if in the -value is positive in the subtree starting in the considered node. If , the variable will be no longer present in , and some lambda-term (described by the type environment) will be substituted for it. For this reason, the information about the -zone and about positivity of the -value is taken from the type environment. Conversely, if , the node (leaf) concerning will be still present in , and thus we can start the branch forming the -zone there. But this is possible only if the node belongs to the -zone; in particular for we need to be in the -zone, which is the case if . Moreover, the total -value in (the subtree starting in) the considered leaf is [math], and thus the productivity order is taken from the environment (unlike in the previous type system).
The rule for lambda-binders realizes a restricted variant of type weakening: we may ignore arguments that do not contain leaves of zones. This is formalized in the notion of balanced and unbalanced type triples, defined by induction on their structure. For , a type triple is -unbalanced if and all elements of the sets are -balanced; otherwise, the type triple is -balanced. A type triple is unbalanced if it is -unbalanced for some ; otherwise it is balanced. Intuitively, a subderivation derives a -unbalanced type triple if the unique leaf of the -zone is contained either in this subderivation, or in an imaginary subderivation that will be substituted for a free variable. Indeed, the subderivation contains the leaf of the -zone if it belongs to the -zone, but none of the arguments provides the leaf.
We can now give the rule; for nodes using this rule, the -value is [math] for all .
[TABLE]
As previously, the rule for application is the most complicated one:
[TABLE]
where
- •
we assume that ;
- •
if there is such that , then we set to , and we say that the -value in the node using such a rule is for all (if there are multiple such , we consider the one for which is the smallest);
- •
otherwise we set to , and the -value to [math] for all .
Let us comment on the above conditions. First, notice that to the subderivation concerning we pass the information about -values and -zones from the subderivations concerning only for (i.e., we write and instead of simply and ). This is because, while thinking about -values and about the -zone, we should imagine the lambda-term obtained from the lambda-term under consideration by reducing all redexes of orders greater than . If , the application (for which we write the rule) is no longer present in (it gets reduced in some of the reductions leading to ), so we should pass the information from to . Conversely, if , the application is still present in ; this means and are independent subterms there, and hence the information from should not be passed to . This is complementary to what we said on the (Var) rule.
Second, we also say for every that only one child can be -unbalanced. Under the intuitive meaning that a conclusion of a subderivation is -unbalanced if the subderivation contains the leaf of the -zone (that remains a leaf in ), this condition ensures that the -zone has at most one leaf, and thus forms a branch in .
Third, observe that the -value in our node is set to if, in , it is the closest ancestor of some node with positive -value that lies in the -zone. Indeed, suppose that the current node is still present in (i.e., that ), and that it belongs to the -zone (i.e., that ). Moreover, suppose that in the -value is positive in some node of the subderivation number (i.e., that ), where . If , then the closest ancestor being in the -zone is already in the subderivation (because its root belongs to the -zone). Conversely, if , the closest ancestor being in the -zone is in our node. Recall that (by definition of type triples) we always have . All the inequalities hold when , and this is exactly the situation when we set the -value of the current node to . If the node is also in the -zone (i.e., if ), then the closest ancestor being in the -zone is in the node itself. It thus makes sense that we also set the -value of the current node to . Repeating this again, we should set to the values of all orders in .
Denoting the -value of a derivation by , we can state the desired properties of our type system.
Theorem 4**.**
The following holds for the type system introduced above:
- (N1*′′*)
if is a homogeneous and closed lambda-term of sort , and is a derivation for , then the number of constants on some branch of the normal form of is at least ; 2. (N2*′′*)
for every there is a function such that if is a homogeneous and closed lambda-term of sort and complexity at most , and on some branch of the beta-normal form of there are appearances of the constant , then there is a derivation for such that .
Example 2**.**
Let us consider the same lambda-term as in Example 1, namely with . As we take its complexity, that is, . Notice that after performing all beta-reductions of order , we obtain the lambda-term with and . In this term, the -zone, which has to be a branch, can descend into one of the subterms , then into one of the subterms , and then it can finish in one of the constants . In effect, while typing , we need two derivations for , one where the lambda-term belongs to the -zone, and one where it does not. Denote . Outside of the -zone, we only pass (from the argument) the information that the -value is positive:
[TABLE]
Notice that in the second (i.e., lower) node using the (@) rule, the function of type , that is , accepts an argument with type triple . This is correct, because according to the (@) rule, the function receives the information only about zones and values of order not greater than the order of the argument, which is [math] in our case, and indeed we have .
Let us now see what happens inside the -zone:
[TABLE]
In the second (i.e., lower) node using the (@) rule, the information about a positive -value (coming from the left subderivation) meets the -zone (coming from the right subderivation), and thus the -value of this node is .
Denoting the type as and as , we continue the derivation for . We choose to start the -zone in a leaf concerning .
[TABLE]
This results in having a node with -value . As we want to continue in the same way with and , we need to derive for and (which describes the situation outside of the -zone):
[TABLE]
We continue as follows, obtaining two more nodes with -value :
[TABLE]
Next we apply the argument , obtaining one more node with -value :
[TABLE]
In the last part of the derivation we also have a node with -value :
[TABLE]
As in Example 1, the total -value of the derivation is , and by adding any further to the sequence , we can increase the -value by .
Example 3**.**
Let us also illustrate on a very simple example how the rule for the constant behaves:
[TABLE]
We thus simply ignore one of the arguments of . Notice that in the second use of the application rule does not require any subderivations for the argument.
Proofs.
Let us now sketch the proof of Theorem 4. Condition (N1*′′*) is based on the following two lemmata.
Lemma 5**.**
Let be a closed lambda-term of sort and complexity at most . If is a derivation for , then there exists a derivation for with .
Lemma 6**.**
Let be a homogeneous and closed lambda-term of sort , and let be an RMF reduction. If is a derivation for , then there exists a derivation for with the same -value.
Condition (N2*′′*) is based on two symmetric lemmata.
Lemma 7**.**
Let be a homogeneous and closed lambda-term of sort , and let be an RMF reduction. If is a derivation for , then there exists a derivation for with the same -value.
Lemma 8**.**
If is a derivation for , then there exists a derivation for with .
Theorem 4 is easily implied. Indeed, consider a homogeneous and closed lambda-term of sort and complexity at most , its normal-form , and lambda-terms such that all reductions between and are RMF.
In Condition (N1*′′*) we start with a derivation for . Then, repeatedly for every we first apply Lemma 5 to (with conclusion ) obtaining a derivation for with -value not smaller than the -value of , and next we apply Lemma 6 to every RMF-reduction between and , obtaining a derivation for with the same -value as . In effect, we obtain a derivation for with -value not smaller than the -value of the original derivation . We conclude by observing that simply follows some branch of , and that its -value equals the number of constants on that branch.
Conversely, while proving Condition (N2*′′*), at the beginning we construct a derivation for , following some branch of ; the -value of this derivation equals the number of constants on the considered branch. Then, repeatedly for every we first apply Lemma 7 for every RMF-reduction between and , obtaining a derivation for with the same -value as , and next we apply Lemma 8 to obtaining a derivation for with -value at most logarithmically smaller than the -value of . In effect, we obtain a derivation for with -value dominating the number of constants on the selected branch of the beta-normal form .
It remains to prove the lemmata. In Lemma 5 we are given a derivation (of order ) concerning a lambda-term of complexity at most . In such a derivation, a node has positive -value (equal ) if it is the closest ancestor of a node with positive -value that is in the -zone (because all variables are of order at most , the information about positive -values is not passed through type environments). Of course every node has only one closest ancestor that is in the -zone, thus the total -value is not greater than the total -value. Having this, we decrease the order of the derivation to , by simply forgetting about -values and about the -zone; the total -value remains unchanged.
Lemmata 6 and 7 can be shown by performing appropriate surgeries on the derivations, like in Section 3. One has to observe there that if a subderivation (for a lambda-term of order ) derives a balanced type triple, then its -value is [math], and its type environment can contain only bindings with balanced type triples. In effect, we can treat subderivations deriving balanced and unbalanced type triples differently. Namely, subderivations deriving balanced type triples can be harmlessly removed or duplicated. Indeed, on the one hand, these operations do not change the total -value. On the other hand, while removing such a subderivation, only bindings with balanced type triples are removed from type environments; this does not cause problems in nodes using the () rule, because this rule allows to drop some balanced type triples. On the other hand, for every the surgery wants to move at most one subderivation deriving a -unbalanced type triple, so no removal or duplication is needed for such subderivations.
In Lemma 8, we have to add an -zone to a derivation of order . Starting from the root of the derivation, we repeatedly descend to the subderivation in which the total -value is the greatest (arbitrarily in the case of a tie); the branch created in this way is taken as the -zone.
If, while descending from some node to its child, the total -value decreases (i.e., either the node itself has -value , or a subderivation starting in some other child also has a positive -value), then the node gets positive -value: it is the closest ancestor of some node with positive -value that is in the -zone. This can happen only in the case of the (@) rule. In the (@) rule one may observe that if a subderivation derives an -balanced type triple for the argument, then its total -value is [math]. We can thus have at most two subderivations (among those starting in children) with positive -value: one for the operand, and one concerning an -unbalanced type triple for the argument. In consequence, while descending to a subderivation, the total -value decreases at most three times (with the exception that it can decrease from to [math]). It follows that the total -value is at least logarithmic in the total -value.
Extension to Recursion Schemes.
Theorem 4 can be also stated for infinite lambda-terms (hence, in particular, for regular infinite lambda-terms represented in a finite way by recursion schemes). The assumption is that we consider there only finite type derivations, and only finite branches of the generated tree (i.e., branches ending in a leaf). Notice that a type derivation for an infinite lambda-term can be finite, because a derivation does not need to descend to every subterm of the lambda-term. We claim that, under these assumptions, Theorem 4 is true for infinite lambda-terms.
To see this, consider a new constant of sort ; it differs from in that we do not have a typing rule for . A cut of a lambda-term is a lambda-term obtained from by replacing some its subterms with lambda-terms of the form (the number of the variables and their sorts are chosen so that the sort of the subterm does not change). It is easy to see that there is a finite derivation for if and only if for some its finite cut there is a derivation for , having the same values (we can cut off subterms not involved in the derivation). Likewise, the tree generated by a closed lambda-term of sort contains some finite branch , if and only if the tree generated by some finite cut of contains the same branch (the finite branch is generated after finitely many beta-reductions, concerning only a top part of , and subterms located deeper in can be cut off). This way, the infinitary version of Theorem 4 can be reduced to the original statement concerning finite lambda-terms.
Because in a single infinite tree we can have branches with arbitrarily many constants , it makes sense to give the following direct corollary of Theorem 4.
Corollary 9**.**
The following conditions are equivalent for a homogeneous and closed (potentially infinite) lambda-term of sort :
- •
for every , in the tree generated by there exists a branch with at least appearances of the constant , and
- •
for every , there exists a derivation for with -value at least .
Because the latter condition is easily decidable for lambda-terms represented by recursion schemes, the corollary implies decidability of the former condition.
Bibliographic Note.
The type system presented in this section is essentially taken from Parys [26]; we have applied some cosmetic changes, though.
In Parys [27] the type system is extended to the task of counting multiple constants: the -value is not a number, but a tuple, where each coordinate of the tuple estimates the number of appearances of a particular constant. In particular, Corollary 9 is extended there to the property “for every , in the tree generated by there exists a branch with at least appearances of every constant from a set ”, giving its decidability. Deciding this property is known under the names simultaneous unboundedness problem (SUP) and diagonal problem (these are two different names for the same problem).
SUP for recursion schemes was first solved in Clemente, Parys, Salvati, and Walukiewicz [9], in a different way. The advantage of solving SUP using the type system presented here is twofold. First, the solution via the type system allows to obtain the optimal complexity, while the complexity of the original solution was much worse. Second, using the type system we can obtain so-called SUP reflection: we can solve SUP simultaneously for all subtrees of the generated tree. More precisely, out of a recursion scheme we can create a new recursion scheme that generates a tree of the same shape as the original one, but such that the label of every node contains additionally the answer to SUP in the subtree starting in that node (i.e., the information whether in that node there start branches with arbitrarily many appearances of every constant from a set ). SUP reflection allowed to solve the model-checking problem for trees generated by recursion schemes against formulae of the WMSO+U logic [29]. This logic extends WMSO (a fragment of MSO in which one can quantify only over finite sets) by the unbounding quantifier, . A formula using this quantifier, , says that holds for arbitrarily large finite sets . Let us also remark that decidability of SUP implies that given a language defined by a nondeterministic recursion scheme, it is possible to compute its downward closure [31], and given two such languages, it is possible to decide whether they can be separated by a piecewise testable language [11].
The type system presented here is also used by Asada and Kobayashi [3] in their work on a pumping lemma for recursion schemes.
The type system was inspired by the previous solution of SUP by Clemente et al. [9]. The idea of having balanced and unbalanced type triples, and treating them differently in type environments, comes from Asada and Kobayashi [2].
5 Branching Quantities
Finally, we shortly mention one more quantity to be considered. In this part, suppose that the constant is of sort , that is, nodes with label have two children. For , let be the full binary tree of height , with all internal nodes labeled by , and all leaves labeled by . We say that embeds homeomorphically in a tree if has a subtree of the form such that embeds in both and (defined by induction); embeds homeomorphically in every tree having a leaf labeled by . Having a tree one may want to find the maximal height of a tree that embeds homeomorphically in . It is an open problem how to estimate this quantity using a type system (or in any other way).
Open Problem 2**.**
Design a type system such that the maximal value (appropriately defined) of a type derivation for a closed lambda-term of sort estimates the maximal number such that embeds homeomorphically in the beta-normal form of .
Like in Section 4 (cf. Corollary 9), existence of such a type system would solve the following problem concerning infinite lambda-terms represented by recursion schemes.
Open Problem 3**.**
Given a recursion scheme, decide whether for every the tree embeds homeomorphically in the (infinite) tree generated by the scheme.
A naive idea is to take the type system from Section 4, and to change the rule for a constant into . Notice, though, that if we derive a type for a tree using such a type system, the value of the derivation counts the maximal number of constants in a tree that embeds homeomorphically in . This is not what we want since, for example, if all are located on a single branch, then their number can be arbitrarily large while only can be embedded. In other words, we add values from the two children of an -labeled node, while we should take their minimum.
It seems that Open Problems 2 and 3 are closely related to the problem of computing the downward closures of languages of finite trees generated by nondeterministic recursion schemes (we remark that the downward closure of every language of finite trees is a regular language, due to the Kruskal’s tree theorem). If we want to compute the downward closure of a language, we have to decide in particular whether it contains trees for all , that is, whether all embed homeomorphically in trees from the language. Like in the case of words, downward closures are also related to the problem of deciding whether two languages can be separated by a piecewise testable language. Goubault-Larrecq and Schmitz [13] derive a general framework for solving the piecewise testable separability for languages of trees.
It is highly probable that Open Problem 3 can be solved for a subclass of recursion schemes, called safe recursion schemes, using methods from Blumensath, Colcombet, Kuperberg, Parys, and Vanden Boom [4]. This requires further investigation.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1]
- 2[2] Kazuyuki Asada & Naoki Kobayashi (2016): On Word and Frontier Languages of Unsafe Higher-Order Grammars . In Chatzigiannakis et al. [ 7 ] , pp. 111:1–111:13, 10.4230/LIP Ics.ICALP.2016.111 . · doi ↗
- 3[3] Kazuyuki Asada & Naoki Kobayashi (2017): Pumping Lemma for Higher-order Languages . In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn & Anca Muscholl, editors: 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland , LIP Ics 80, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 97:1–97:14, 10.4230/LIP Ics.ICALP.2017.97 . · doi ↗
- 4[4] Achim Blumensath, Thomas Colcombet, Denis Kuperberg, Paweł Parys & Michael Vanden Boom (2014): Two-Way Cost Automata and Cost Logics over Infinite Trees . In Thomas A. Henzinger & Dale Miller, editors: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014 , ACM, pp. 16:1–16:9, 10.1145/2603088.2603104 . · doi ↗
- 5[5] Christopher H. Broadbent, Arnaud Carayol, Matthew Hague & Olivier Serre (2012): A Saturation Method for Collapsible Pushdown Systems . In Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts & Roger Wattenhofer, editors: Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II , Lecture Notes in Computer Science 7392, Springer, pp. 165–176, 10.1007/978-3-642-31585-5_18 . · doi ↗
- 6[6] Christopher H. Broadbent & Naoki Kobayashi (2013): Saturation-Based Model Checking of Higher-Order Recursion Schemes . In Simona Ronchi Della Rocca, editor: Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy , LIP Ics 23, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 129–148, 10.4230/LIP Ics.CSL.2013.129 . · doi ↗
- 7[7] Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani & Davide Sangiorgi, editors (2016): 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy . LIP Ics 55, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
- 8[8] Lorenzo Clemente, Paweł Parys, Sylvain Salvati & Igor Walukiewicz (2015): Ordered Tree-Pushdown Systems . In Prahladh Harsha & G. Ramalingam, editors: 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India , LIP Ics 45, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 163–177, 10.4230/LIP Ics.FSTTCS.2015.163 . · doi ↗