arXiv:cs/0405085v1 [] 24 May 2004

On the Expressive Power of First-Order Boolean Functions in
PCF∗
Prakash Panangaden
School of Computer Science
McGill University
Montreal H3A 2K7, Canada

Riccardo Pucella
Department of Computer Science
Cornell University
Ithaca, NY, 14853, USA

Abstract
Recent results of Bucciarelli show that the semilattice of degrees of parallelism of firstorder boolean functions in PCF has both infinite chains and infinite antichains. By considering
a simple subclass of Sieber’s sequentiality relations, we identify levels in the semilattice and
derive inexpressibility results concerning functions on different levels. This allows us to further
explore the structure of the semilattice of degrees of parallelism: we identify semilattices characterized by simple level properties, and show the existence of new infinite hierarchies which
are in a certain sense natural with respect to the levels.

1 Introduction
In this paper we study the relative definability of first-order boolean functions with respect to
Plotkin’s language PCF [9], a simply-typed λ-calculus with recursion over the ground types of integers and booleans. Relative definability defines a preorder on continuous boolean functions, and
this ordering induces a natural equivalence relation. The object of our study will be the structure of
the resulting partially ordered set of equivalence classes of functions (called degrees of parallelism).
Work by Trakhtenbrot [16, 17], Sazonov [13], Lichtenthäler [7] and Bucciarelli and Malacaria [2, 5]
show that the structure of degrees of parallelism is highly non-trivial: even when restricted to firstorder functions, the poset forms a sup-semilattice and contains a ”two-dimensional” hierarchy of
functions, both infinite chains and infinite antichains of functions.
It is known that the definability ordering is completely characterized by the sequentiality relations of Sieber. The result is a duality of sorts: f can be defined using g if the sequentiality
relations under which g is invariant is a subset of the sequentiality relations under which f is invariant. Therefore, it seems worthwhile to try to derive the set of sequentiality relations under which a
given function is invariant. As a first step towards this goal we focus our attention in this paper on
a simple class of sequentiality relations we call presequentiality relations. Invariance under presequentiality relations induces a coarser ordering on functions than full sequentiality relations, from
∗

This paper is essentially the same as one that appeared in Theoretical Computer Science 266(1-2), pp. 543-567,
2001. This work was done while the first author was at McGill University, and was supported in part by a scholarship
from FCAR. A preliminary version of this paper was written while the first author was at Bell Laboratories, Lucent
Technologies.

1

which we cannot infer definability results but can infer strong inexpressibility results. In effect, this
coarser ordering is a “skeleton” of the definability preorder.
The main advantage of working with presequentiality relations is that we can completely characterize the set of presequentiality relations under which a given function is invariant. It turns out that
a pair of integers is sufficient to completely describe this set. This pair of integers, called the presequentiality level of the function, can straightforwardly be derived from the trace of the function.
Well-known functions in the definability preorder, such as Parallel OR, the Berry-Plotkin function,
the Gustave function, the Detector function, can be easily characterized in terms of presequentiality levels. We use presequentiality levels to guide our exploration of the definability preorder: we
present subsemilattices with natural presequentiality level characterizations, namely the stable, unstable, stable-dominating and monovalued functions. We exhibit natural hierarchies of functions in
these lattices, where natural is taken to mean that every function in the hierarchy has a different
presequentiality level, thereby making the hierarchy part of the skeleton of the definability preorder.
This paper is structured as follows. In the next section, we review the required mathematical
preliminaries, rigorously defining the notions of relative definability, traces, linear coherence, as
well as stating useful existing results. In Section 3, we study presequentiality relations, and prove
the two main lemmas of this paper: the Reduction Lemma and the Closure Lemma, which allow us
to find canonical representatives for the set of presequentiality relations under which a function is
invariant. In Section 4, we point out the relationship between the canonical representatives and the
trace of the function, and thus define the notion of presequentiality level. Section 5 then investigates
the structure of the definability preorder guided by presequentiality levels, as described above.
This work is in the lineage of the work of Bucciarelli in [2] and Bucciarelli and Malacaria in
[5]. The main results from this paper were originally reported in [11].

2 Preliminaries
In this section, we review some of the mathematical background to our study of first-order monotone
boolean functions and the previous work already done on the subject by Trakhtenbrot, Sazanov,
Bucciarelli and Malacaria. We assume knowledge of PCF and its continuous model [9], as well
as a passing familiarity with logical relations [10]. Let B be the flat domain of boolean values.
Given
f : B k → B and x = (x1 , . . . , xk ),then f (x) stands for f (x1 , . . . , xk ), and given A =
 1
x , . . . , xn ⊆ B k , f (A) is defined to be f (xi ) : xi ∈ A . As usual, π1 and π2 represent the
projection functions associated with the cartesian product on sets.
Relative definability refers to the ability to define some function using another function: a function can define another function if there exist some algorithm in some language that uses the former
to compute the latter. In our case, algorithms are taken to be PCF-terms: given two continuous
functions f and g, we say that f is PCF-expressible (or simply expressible) by g, denoted f  g,
if there exists a PCF-term M such that f = M g. Equivalent terminologies in the literature for
f  g are “f is less parallel than g”, or f is g-expressible. The  preorder induces an equivalence
relation ≡ on continuous function such that f ≡ g iff f  g and g  f . The equivalence classes are
called degrees of parallelism, and two functions f ,g with f ≡ g are called equiparallel. The degree
of parallelism of a continuous function f is denoted [f ].
We are interested in studying the structure of first-order degrees of parallelism. Trakhtenbrot
[16, 17] and Sazonov [13] first investigated the subject and pointed out finite subposets of degrees

2

(though not necessarily first-order degrees). Some facts are consequences of well-known results.
The poset of degrees of parallelism must have a top element, Parallel OR (POR), by Plotkin’s full
abstraction result for PCF+POR [9]. On the other hand, the poset must have a bottom element, the
degree of all M-sequential functions. Indeed, a fundamental property of PCF is that PCF-definable
functions are exactly the M-sequential functions. A function f : B k → B is M-sequential [8] (or
simply sequential) if it is constant or if there exists an integer i (called an index of sequentiality)
with 1 ≤ i ≤ k such that xi = ⊥ implies that f (x1 , . . . , xk ) = ⊥ and such that for any fixed value
xi , the function of the remaining arguments is also M-sequential. In [5], it is proved that first-order
degrees of parallelism form a sup-semilattice, which we will denote CONT1.
Proposition 2.1 The poset of first-order degrees of parallelism is a sup-semilattice with a bottom
element (the set of sequential functions) and a top element (the degree of POR).
The trace of a function is the central notion we use to study boolean functions. The trace is a
representation of the minimum inputs needed for the function to produce a result. Formally, given a
first-order monotone function f : B k → B, the trace of f is
n

tr(f ) = (v, b)|v ∈ B k , b ∈ B, b 6= ⊥, f (v) = b and ∀v ′ < v, f (v ′ ) = ⊥

o

For x, y ∈ B, let x ↑ y hold if x and y have a common upperbound in B, that is if x = ⊥ or y = ⊥
or x = y. Extend ↑ pointwise to tuples in B n . It is easy to see that a first-order monotone boolean
function f is stable (in the sense of Berry [1]) if and only if for all v1 , v2 ∈ π1 (tr(f )), v1 6↑ v2 . Note
that the monotonicity of f insures that if v1 ↑ v2 then f (v1 ) = f (v2 ). For a set of tuples A ⊆ B k ,
a set B ⊆ B k is an Egli-Milner lowerbound for A if for every x ∈ A, there is a y ∈ B with y ≤ x,
and for every y ∈ B, there is an x ∈ A with y ≤ x.
Linear coherence is used
by Bucciarelli and Erhard to study first-order boolean functions in
 1
[3, 4, 2]. A subset A = v , . . . , v n of B k is linearly coherent (or simply coherent) if for every
coordinate, either a tuple in A contains ⊥ at that coordinate, or all the tuples in A have the same
value at that coordinate, that is




∀j ∈ {1, . . . , k} ∀l ∈ {1, . . . , n}, vjl 6= ⊥ ⇒ ∀l1 , l2 ∈ {1, . . . , n}, vjl1 = vjl2


A subset A = v 1 , . . . , v n of B k is ⊥-covering if for every coordinate a tuple in A contains ⊥ at
that coordinate, that is
∀j ∈ {1, . . . , k}, ∃i ∈ {1, . . . , k}, vji = ⊥
It is easy to see that if A is ⊥-covering then A is coherent. Abusing the terminology, we will
sometimes say that a first-order monotone boolean function f is ⊥-covering if π1 (tr(f )) has the
corresponding property.
Monovalued functions are an important class of functions we study. A first-order monotone
boolean function f is monovalued if |π2 (tr(f ))| = 1. By another abuse of terminology, we will
say that a subset A ⊆ π1 (tr(f )) is monovalued if |f (A)| = 1. A boolean function which is not
monovalued will sometimes be called bivalued2 .
1

CONT refers to the fact that those functions are continuous: recall that for first-order boolean functions, monotone
functions are continuous.
2
The term “bivalued” refers of course to the fact that there are two non-⊥ values in the boolean domain — a function
is bivalued if |π2 (tr(f ))| = 2.

3

We define two operations on boolean functions. Given a first-order monotone boolean function
f : B k → B, let neg(f ) : B k → B be the function returning tt when f returns ff and returning ff
when f returns tt. As for the second operation, given two first-order monotone boolean functions
′
f : B k → B and g : B k → B, (without loss of generality, assume there exists an l ≥ 0 with
′
k = k′ + l) define the function f + g : B max(k,k )+1 → B by the following trace:
tr(f + g) = {((tt, x1 , . . . , xk ), b) : ((x1 , . . . , xk ), b) ∈ tr(f )}

[

{((ff, . . . , ff, x1 , . . . , xk′ ), b) : ((x1 , . . . , xk′ ), b) ∈ tr(g)}
| {z }
l+1

As shown in [5], f + g is equiparallel to the least upperbound of f and g in CONT, in other words
[f + g] = [f ] ∨ [g].
Bucciarelli illustrates the non-trivial structure of the CONT semilattice by exhibiting hierarchies3 of functions in CONT [2]. He defines the function BUCC(n,m) via the following description: the trace of BUCC(n,m) has m elements and each trace element returns tt; for any subset of
less than n elements (and at least two) of the first projection of the trace, there exists a coordinate
which makes that subset incoherent. The Bucciarelli hierarchy is actually a two-dimensional infinite
hierarchy of functions.
Generalizing the techniques used in [2], Bucciarelli and Malacaria prove the following proposition in [5], in their attempt to find a characterization of the CONT semilattice in terms of hypergraphs (this proposition is restated so that it does not refer to hypergraphs)
Proposition 2.2 (Bucciarelli, Malacaria) Let f, g be two first-order monotone boolean functions.
If there exists a function α : tr(f ) → tr(g) such that
1. for all A ⊆ tr(f ), if π1 (A) is non-singleton and linearly coherent, then π1 (α(A)) is nonsingleton and linearly coherent.
2. for all A ⊆ tr(f ) with π1 (A) non-singleton and linearly coherent, and for all x, y ∈ A, we
have π2 (x) 6= π2 (y) ⇒ π2 (α(x)) 6= π2 (α(y)).
then f  g.
This property will be used often in this paper to prove definability results between functions.

3 Presequentiality relations
Relative definability for first-order boolean functions is fully characterized by Sieber’s sequentiality
relations, introduced in [14]. Sequentiality relations are the logical relations [10] under which the
constants of PCF are invariant. Recall that an n-ary logical relation R on a λ-model (D τ )t∈Type is a
family of relations Rτ ⊆ (D τ )n such that for all types σ, τ and f1 , . . . , fn ∈ D σ→τ ,
Rσ→τ (f1 , . . . , fn ) ⇔ ∀d1 , . . . , dn , Rσ (d1 , . . . , dn ) ⇒ Rτ (f1 d1 , . . . , fn dn )
An element d ∈ D τ is invariant under R if Rτ (d, . . . , d) holds. We now give the definition of
sequentiality relations in a slightly different form than Sieber in [14], distinguishing the simple kind
of sequentiality relations which we call presequentiality relations.
3

A hierarchy is simply an ω-chain in the definability preorder.

4

Definition 3.1 For each n ≥ 0 and each pair of sets A ⊆ B ⊆ {1, . . . , n}, the presequentiality
relation SnA,B ⊆ (D τ )n , τ = ι, o, is an n-ary logical relation defined by
SnA,B (d1 , . . . , dn ) ⇔ (∃i ∈ A.di = ⊥) ∨ (∀i, j ∈ B.di = dj )
An n-ary logical relation R is called a sequentiality relation if R is an intersection of presequentiality relations.
Sieber’s relations are defined for full PCF, that is with both integers (type ι) and booleans
(type o). For the purposes of this paper, it is sufficient to look at relations over the booleans,
that is over B = D o . For the special case of a first-order boolean function f : B k → B,
invariance
under SnA,B means thatfor tuples (x11 , . . . , x1n ), . . . , (xk1 , . . . , xkn ) in SnA,B , we have

1
f (x1 , . . . , xk1 ), . . . , f (x1n , . . . , xkn ) also in SnA,B . The following proposition, proved in [14], gives
the full characterization of the definability preorder for first-order functions. It is interesting to note
that this characterization is effective and Stoughton implemented an algorithm that decides f  g
given the functions f and g [15].
Proposition 3.2 (Sieber) For any first-order monotone boolean functions f and g, f  g if and
only if for any sequentiality relation R, if g is invariant under R then f is also invariant under R.
Proposition 3.2 tells us that a function f is not g-expressible if we can exhibit a sequentiality
relation R such that g is invariant under R but f is not. If we restrict our attention to presequentiality
relations, it is easy to see that invariance under presequentiality relations induces a coarser ordering
than invariance under sequentiality relations, that is it identifies more functions. If two functions
are invariant under the same presequentiality relations, then nothing can be said about their relative
definability. However, if they are not invariant under the same presequentiality relations, we can derive strong inexpressibility results, since presequentiality relations are a weak class of sequentiality
relations. In effect, invariance under presequentiality relations can be viewed as defining the “skeleton” of the relative definability preorder. The advantage of working with presequentiality relations
is that they are simpler than full sequentiality relations, and a great deal of structure can be extracted
straightforwardly, as we will presently see.
The central problem of this paper is to determine the presequentiality relations under which
a given function is invariant. An early restricted form of this may already be found in [2]. The
following two lemmas show that it is not necessary to consider every presequentiality relation.
The Reduction Lemma tells us that it is sufficient to look at presequentiality relations of a simple
form. The Closure Lemma says that if a function is invariant under a presequentiality relation SnA,B ,
invariance holds under any presequentiality relation with “smaller” A and B. In Section 4, we will
see how these lemmas lead to a simple characterization of the set of presequentiality relations under
which a function is invariant.
Lemma 3.3 (Reduction Lemma) Given f : B k → B a first-order monotone boolean function and
A ⊆ B ⊆ {1, . . . , n}, one of the following holds:
{1,...,|A|},{1,...,|A|}

1. (A = B) f is invariant under SnA,A ⇔f is invariant under S|A|

{1,...,|A|},{1,...,|A|+1}

2. (A ⊂ B) f is invariant under SnA,B ⇔f is invariant under S|A|+1
5

.

Lemma 3.4 (Closure Lemma) Given f : B k → B a first-order monotone boolean function and m
any integer with m ≥ 0, the following holds:
{1,...,m},{1,...,m+1}

1. f invariant under Sm+1

{1,...,m},{1,...,m}

⇒ f invariant under Sm

{1,...,m+1},{1,...,m+1}

⇒ f invariant under Sm

{1,...,m+1},{1,...,m+2}

⇒ f invariant under Sm+1

2. f invariant under Sm+1
3. f invariant under Sm+2

.

{1,...,m},{1,...,m}

{1,...,m},{1,...,m+1}

The proof of these lemmas is much more digestible when split across several technical lemmas
(3.5,3.6,3.7) which we now state and prove.
Lemma 3.5 Let m(M ) be the least n such that M ⊆ {1, . . . , n}, and let f : B k → B be a firstorder monotone boolean function. The function f is invariant under SnA,B iff f is invariant under
A,B
Sm(B)
.
Proof. (⇒) We show that if f is invariant under SnA,B , then for all n′ ≤ n such that B ⊆
.
{1, . . . , n′ }, f is invariant under SnA,B
′
For the sake of contradiction, assume there exist n, A, B, n′ with n′ ≤ n such that
 f is invariant


1 , . . . , x1 , · · · , xk , . . . , xk
.
That
is,
there
exist
tuples
x
under SnA,B but not under SnA,B
∈
′
′
′
1
1
n
n
with yi = f (x1i , . . . , xki ).
and (y1 , . . . , yn′ ) 6∈ SnA,B
SnA,B
′
′
The tuples
(x11 , . . . , x1n′ , ⊥, . . . , ⊥), · · · , (xk1 , . . . , xkn′ , ⊥, . . . , ⊥)

, we must have (y1 , . . . , yn′ , ⊥, . . . , ⊥) 6∈ SnA,B ,
then must be in SnA,B . Since (y1 , . . . , yn′ ) 6∈ SnA,B
′
A,B
contradicting the invariance of f under Sn .
.
(⇐) We show that if f is invariant under SnA,B , then for all n′ ≥ n, f is invariant under SnA,B
′
′
For the sake of contradiction, assume there exist n, A, B and n ≥ n such that
 f is invariant


1 , . . . , x1 , · · · , xk , . . . , xk
under SnA,B but not under SnA,B
.
That
is,
there
exist
tuples
x
∈
′
1
1
n′
n′

⇔
that (x1 , . . . , xn′ ) ∈ SnA,B
with yi = f (x1i , .. . , xki ). Observe
SnA,B
and (y1 , . . . , yn′ ) 6∈ SnA,B
′
′
′


1
k
A,B
1
k
A,B
A,B
(x1 , . . . , xn ) ∈ Sn . Hence, x1 , . . . , xn , · · · , x1 , . . . , xn ∈ Sn but (y1 , . . . , yn ) 6∈ Sn

contradicting the invariance of f under SnA,B .

⊔
⊓

Lemma 3.6 Given f : B k → B a first-order monotone boolean function, f is invariant under SnA,B
{1,...,|A|},{1,...,|B|}
iff f is invariant under Sn
.
Proof.
We show the following more general result: let A, B, C, D be sets with A ⊆ B ⊆
{1, . . . , n} , C ⊆ D ⊆ {1, . . . , n}, and let p be a permutation of {1, . . . , n} into {1, . . . , n} such
that p(A) = C and p(B) = D. Then f is invariant under SnA,B ⇔f is invariant under SnC,D .
Let us first prove that
(x1 , . . . , xn ) ∈ SnA,B ⇔ (xp−1 (1) , . . . , xp−1 (n) ) ∈ SnC,D .

(1)

Let (x1 , . . . , xn ) ∈ SnA,B , and yi = xp−1 (i) . To show (y1 , . . . , yn ) ∈ SnC,D , consider the two cases:

6

1. There is an i ∈ A, xi = ⊥. In which case, let c = p(i), with c ∈ C since i ∈ A. Moreover,
yc = xp−1 (c) = xp−1 (p(i)) = xi = ⊥, so there is a j ∈ C, yj = ⊥.
2. For all i, j ∈ B, xi = xj . Assume there are i, j ∈ D, yi 6= yj . Then xp−1 (i) 6= xp−1 (j) , hence
there are i′ , j ′ ∈ B, xi′ 6= xj ′ , a contradiction. Hence for all i, j ∈ D, yi = yj .
Hence (y1 , . . . , yn ) ∈ SnC,D . The reverse direction follows by symmetry of the permutation p,
proving (1).
Now, observe that we need only show one direction of the general result (the reverse direction
follows by symmetry of the permutation p).


Consider any tuples x11 , . . . , x1n , · · · , xk1 , . . . , xkn ∈ SnA,B . Let yi = f (x1i , . . . , xki ). Since f

is invariant under SnA,B ,(y1 , . . . , yn) ∈ SnA,B .
By (1), each tuple xj1 , . . . , xjn is also in SnC,D and so is (y1 , . . . , yn ) ∈ SnC,D , hence f is

invariant under SnC,D .
To prove the lemma, it is sufficient to show that there exists a permutation p of {1, . . . , n} such
that p(A) = {1, . . . , |A|}, p(B) = {1, . . . , |B|}, which is immediate.
⊔
⊓

Lemma 3.7 Given f : B k → B a first-order monotone boolean function. Then f is invariant under
′
SnA,B , |B\A| = 1 iff f is invariant under SnA,B for any B ′ such that B ⊆ B ′ .
Proof. (⇒) We show that if f is invariant under SnA,B , |B\A| = 1, then for any B ′ such that
′
B ⊆ B ′ , f is invariant under SnA,B .
By Lemma 3.5 and Lemma 3.6, it is sufficient to show that for any m, if f invariant under
{1,...,m},{1,...,m+1}
{1,...,m},{1,...,n}
Sm+1
then f is invariant under Sn
for any n ≥ m + 1.
For the sake of contradiction, assume that for some m and n ≥ m + 1, f is invariant under
{1,...,m},{1,...,m+1}
{1,...,m},{1,...,n}
the presequentiality relation
Sm+1 
but not under Sn
. Then there are

{1,...,m},{1,...,n}



tuples x11 , . . . , x1n , · · · , xk1 , . . . , xkn ∈ Sn

{1,...,m},{1,...,n}

but (y1 , . . . , yn ) 6∈ Sn

, for

yi = f (x1i , . . . , xki ). Hence, for all i ≤ m, yi 6= ⊥ and there are I, J such that yI 6= yJ . Without
loss of generality, choose I the minimal such index.
We proceed by case analysis on the value of I and J:






1. (I ≤ m) Consider the following tuples x11 , . . . , x1m , x1J , · · · , xk1 , . . . , xkm , xkJ which are
{1,...,m},{1,...,m+1}

in Sm+1

; by assumption of the invariance of f , we have (y1 , . . . , ym , yJ ) ∈

{1,...,m},{1,...,m+1}
Sm+1

Hence, either there is i ≤ m such yi = ⊥ (a contradiction), or yI = yJ
(also a contradiction).
2. (J ≤ m) Same argument.
3. (I, J > m) We further consider 3 subcases.






(a) (yI = ⊥). Consider the tuples x11 , . . . , x1m , x1I , . . . , xk1 , . . . , xkm , xkI which are in
{1,...,m},{1,...,m+1}

Sm+1

; by assumption of the invariance of f we have (y1 , . . . , ym , yI ) ∈

{1,...,m},{1,...,m+1}
Sm+1
.

So either there is i ≤ m such that yi = ⊥ (a contradiction), or
yI = yi for all i ≤ m (also a contradiction)
7

(b) (yJ = ⊥) Same argument.
(c) (yI , yJ 6= ⊥) By choice of minimal I, we know that y1 = · · · = ym and all are either tt
or ff. On the other hand, yI 6= yJ and yI , yJ 6= ⊥, so let c =I or J, such that yc 6= y1 .

Consider the tuples x11 , . . . , x1m , x1c , · · · , xk1 , . . . , xkm , xkc , easily seen to be tuples in
{1,...,m},{1,...,m+1}

Sm+1

, and by assumption of the invariance of f , we have (y1 , . . . , ym , yc ) ∈

{1,...,m},{1,...,m+1}
.
Sm+1

So either there is an i ≤ m such that yi = ⊥ (a contradiction), or
yc = y1 (also a contradiction)
′

(⇐) We show that if f is invariant under SnA,B , then f is invariant under SnA,B for all A ⊆
′
B ⊆ B.
For the sake of contradiction, assume there exist n, A, B, B ′ with A ⊆ B ′ ⊆ B such
 that f isin
′
1
A,B
A,B
1
variant under Sn but not under Sn . Then there exist tuples x1 , . . . , xn , · · · , xk1 , . . . , xkn ∈
′

′

SnA,B such that (y1 , . . . , yn ) 6∈ SnA,B with yi = f (x1i , . . . , xki ).

Fix an arbitrary I ∈ A. Consider the following tuples: z1j , . . . , znj for 1 ≤ j ≤ k, with
zij



=

 j

 xi



xjI
⊥

if i ∈ B ′
if i ∈ B\B ′
otherwise

We first verify that these tuples are in SnA,B . For each j, 1 ≤ j ≤ k, consider the original tuple
′
xj1 , . . . , xjn ∈ SnA,B . In other words, either




1. there is an i ∈ A, xji = ⊥, and for that i ∈ A, we have zij = xji = ⊥. Hence z1j , . . . , znj ∈
SnA,B , or

2. For all i ∈ A, xji 6= ⊥, and for all i, i′ ∈ B ′ , xji = xji′ . Hence, for all i, i′ ∈ B ′ , zij = zij′ .
Moreover, for all i ∈B\B ′ , zij = xjI for I ∈ A ⊆ B ′ . Hence, for all i, i′ ∈ B, zij = zij′ and
the tuple z1j , . . . , znj ∈ SnA,B .

By the above construction, we see that for all i ∈ B ′ , f (zi1 , . . . , zik ) = yi .
′
Since (y1 , . . . , yn ) 6∈ SnA,B , we have for all i ∈ A, yi 6= ⊥ and there are i, j ∈ B ′ , yi 6= yj . This
implies that for all i ∈ A, f (zi1 , . . . , zik ) 6= ⊥ and there are i, j ∈ B ′ ⊆ B such that f (zi1 , . . . , zik ) 6=
⊔
⊓
f (zj1 , . . . , zjk ). In other words, f is not invariant under SnA,B , contracting the assumption.
The proofs of the Reduction and Closure Lemmas are now immediate.
Proof. (Reduction Lemma)
1. (A = B) By Lemma 3.6, we have that f is invariant under SnA,A iff f is invariant under
{1,...,|A|},{1,...,|A|}
{1,...,|A|},{1,...,|A|}
Sn
and by Lemma 3.5, f is invariant under Sn
iff f is invariant
{1,...,|A|},{1,...,|A|}
under S|A|
.
2. (A ⊂ B) By Lemma 3.6, f is invariant under SnA,B iff f is invariant under
{1,...,|A|},{1,...,|B|}
{1,...,|A|},{1,...,|B|}
Sn
. By Lemma 3.7, f is invariant under Sn
iff f is invari{1,...,|A|},{1,...,|A|+1}
ant under Sn
, and by Lemma 3.5, this happens iff f is invariant under
{1,...,|A|},{1,...,|A|+1}
S|A|+1
.
⊔
⊓
8

Proof. (Closure Lemma)
1. The (⇐) direction in the proof of Lemma 3.7 actually proves this case.






{1,...,m},{1,...,m}

2. Given tuples x11 , . . . , x1m , · · · , xk1 , . . . , xkm ∈ Sm
{1,...,m},{1,...,m}

Sm

with yi = f (x1i , . . . , xki ).





we show (y1 , . . . , ym ) ∈



{1,...,m+1},{1,...,m+1}

By assumption, the tuples x11 , . . . , x1m , x11 , · · · , xk1 , . . . , xkm , xk1 are in Sm+1
By invariance of f
{1,...,m+1},{1,...,m+1}
Sm+1

{1,...,m+1},{1,...,m+1}

under Sm+1

,

we have (y1 , . . . , ym , y1 )

∈

which means that either there is i ≤ m such that yi = ⊥ or for
{1,...,m},{1,...,m}

all i, j ≤ m, yi = yj . Hence (y1 , . . . , ym ) ∈ Sm



.
{1,...,m},{1,...,m+1}

3. Same argument as part (2): assume tuples
xi1 , . . . , xim+1 in Sm+1

sider the tuples xi1 , . . . , xim , xi1 , xim+1 .

, and con⊔
⊓

4 Presequentiality levels
The Reduction Lemma and the Closure Lemma of the previous section can be used to show that the
set of presequentiality relations under which a function is invariant is characterized by two integers
(allowing for ∞). Given f a function invariant under presequentiality relations {SnAi ,Bi }i∈I ; by the
Reduction Lemma, this is equivalent to saying that f is invariant under the presequentiality relations
{1,...,|A |},{1,...,|Ai |+1}
{1,...,|A |},{1,...,|Ai |}
}i∈I,Ai ⊂Bi . By the Closure Lemma,
{S|Ai | i
}i∈I,Ai =Bi and {S|Ai |+1 i
{1,...,k},{1,...,k}

for
there must exist maximal i and j (possibly ∞) such that f is invariant under Sk
{1,...,k},{1,...,k+1}
for all k ≤ j. We will call the pair (i, j) the
all k ≤ i and f is invariant under Sk+1
presequentiality level (p-level) of the function f . Clearly, a function with a p-level of (∞, ∞) is
invariant under all presequentiality relations. Since every function in a degree of parallelism must
be invariant under the same presequentiality relations (by Proposition 3.2), we also talk about the
presequentiality level of a degree of parallelism. Alternatively, a function with a p-level of (i, j) is
easily seen by applications of the Reduction Lemma and the Closure Lemma to be invariant under
a presequentiality relation SnA,B if and only if either |A| = |B| ≤ i or |A| < |B| with |A| ≤ j.
In view of the discussion following Proposition 3.2, no definability information can be inferred
for two functions with the same p-level. However, functions with different p-levels yield immediate
inexpressibility results:
Corollary 4.1 Given f and g first-order monotone boolean functions with p-levels of (if , jf ) and
(ig , jg ) respectively. If if > ig or jf > jg , then g 6 f .
In summary, two integers are sufficient to completely characterize the set of presequentiality
relations under which a function is invariant. It turns out that these integers can be derived straightforwardly from the trace of the function. Define the coefficient of (linear) coherence of a first-order
monotone boolean function f by
cc(f ) = min {|A| : A ⊆ π1 (tr(f )), |A| ≥ 2, A coherent}
9

.

with cc(f ) defined to be ∞ when π1 (tr(f )) has no non-singleton linearly coherent subset. Similarly,
define the bivalued coefficient of (linear) coherence of a first-order monotone boolean function f by
bcc(f ) = min {|A| : A ⊆ π1 (tr(f )), |A| ≥ 3, A coherent and bivalued}
with bcc(f ) is defined to be ∞ when π1 (tr(f )) has no non-singleton bivalued linearly coherent
subset. We note that bcc(f ) ≥ cc(f ) for all f .
The relationship between coefficients of coherence and presequentiality levels is expressed by
the following proposition, which provides a mechanical way of determining the presequentiality
level of a function, and hence of determining the set of presequentiality relations under which a
function is invariant.
Lemma 4.2 Let f : B k → B be a first-order monotone boolean function. Then f has a p-level of
(bcc(f ) − 1, cc(f ) − 1) (assuming standard rules for ∞).
Proof. We prove the result for cc(f ). Consider the three cases:
{1},{1,2}

{1,2},{1,2,3}

1. (cc(f ) = 2) We show that f is invariant under S2
but not S3 
 . Assume f

{1},{1,2}
{1},{1,2}
k
k
1
1
. Then there exist tuples x1 , x2 , · · · , x1 , x2 ∈ S2
is not invariant under S2
{1},{1,2}

, with yi = f (x1i , . . . , xki ). This means that y1 6= ⊥ and
such that (y1 , y2 ) 6∈ S2
y1 6= y2 . It is easy to see that (x11 , . . . , xk1 ) ≤ (x12 , . . . , xk2 ), since for each i ≤ k, either
xi1 = ⊥ or xi1 = xi2 . So by monotonicity of f , y1 ≤ y2 , contradicting y1 6= ⊥, and
{1},{1,2}
. On the other hand, applying f to the tuples
y1 6= y2 . So f must
 under S2
 be invariant

{1,2},{1,2,3}
k
k
1
1
, where the first two coordinates of the tuples
x1 , x2 , ⊥ , · · · , x1 , x2 , ⊥ ∈ S 3
are the elements of the first projection of the trace forming a linearly coherent subset of size
{1,2},{1,2,3}
2, yields the tuple (tt, tt, ⊥) or (ff, ff, ⊥), neither of which is in S3
.
{1,...,cc(f )−1},{1,...,cc(f )}

2. (3 ≤ cc(f ) < ∞) We show f is invariant under Scc(f )
{1,...,cc(f )},{1,...,cc(f )+1}

Scc(f )+1



but not under

{1,...,cc(f )−1},{1,...,cc(f )}

. Assume f is not invariant under Scc(f )


. Then





{1,...,cc(f )−1},{1,...,cc(f )}
such
there exist tuples x11 , . . . , x1cc(f ) , · · · , xk1 , . . . , xkcc(f ) ∈ Scc(f )


{1,...,cc(f )−1},{1,...,cc(f )}
k
1
with yi = f (xi , . . . , xi ). This means that
that y1 , . . . , ycc(f ) 6∈ Scc(f )

for all i ≤ cc(f ) − 1, yi 6= ⊥ and there are I, J with yI 6= yJ . Let C ⊆ π1 (tr(f )) be an
Egli-Milner lowerbound of the first cc(f )−1 coordinates of the given tuples, |C| ≤ cc(f )−1.
We cannot have |C| = 1 (say C = {v}), since that would imply that v ≤ (x1cc(f ) , . . . , xkcc(f ) ):
for each i ≤ k, either one of xij = ⊥ for j ≤ cc(f ) − 1 (hence vj = ⊥) or xij = xij ′ for all
j, j ′ ≤ cc(f ) − 1 (hence vj ≤ xij = xicc(f ) ). But monotonicity of f would imply that for all
i, j, yi = yj , a contradiction. Hence, |C| ≥ 2. But since the first cc(f ) − 1 coordinates of the
given tuples form a coherent subset, C being an Egli-Milner lowerbound must also be coherent (by a result in [2]). But this contradicts the fact that the minimal size for a coherent subset
{1,...,cc(f )−1},{1,...,cc(f )}
of π1 (tr(f )) is cc(f ). So, f is invariant under Scc(f )
. On the other hand,








{1,...,cc(f )},{1,...,cc(f )+1}

consider the tuples x11 , . . . , x1cc(f ) , ⊥ , · · · , xk1 , . . . , xkcc(f ) , ⊥ ∈ Scc(f )+1
where the first cc(f ) coordinates are the elements of a coherent subset of size cc(f )
of π1 (tr(f )) (which exists by assumption). Appplying f to these tuples yields a tuple
{1,...,cc(f )},{1,...,cc(f )+1}
(y1 , . . . , ycc(f ) , ⊥) with yi 6= ⊥ for i ≤ cc(f ), which cannot be in Scc(f )+1
.
10

3. (cc(f ) = ∞) We show that f is invariant under all presequentiality relations of the
{1,...,i},{1,...,i+1}
form Si+1
. Assume that there exists an i such that f is not invariant under
{1,...,i},{1,...,i+1}

Si+1
. The same reasoning as in the previous case leads to a contradiction, although instead of contradicting the minimal size of a coherent subset of π1 (tr(f )) being
cc(f ), we contradict the fact that there is no coherent subset of π1 (tr(f )).
The argument for bcc(f ) is similar.

⊔
⊓

We can use Lemma 4.2 to show that presequentiality levels are preserved by the least upperbound operation on functions in a natural way:
Lemma 4.3 Given f and g first-order monotone boolean functions with p-levels of (if , jf ) and
(ig , jg ) respectively. Then the p-level of f + g is
(min(if , ig ), min(jf , jg ))
.
Proof. Immediate by Lemma 4.2 and the definition of f + g in terms of f and g.

⊔
⊓

It is not hard to check that any first-order monotone boolean function has a p-level (i, j) with
i ≥ 2 and j ≥ 1 (consider 3 cases: cc(f ) = ∞, cc(f ) < ∞ = bcc(f ), bcc(f ) < ∞). We can
easily characterize sequential functions:
Proposition 4.4 A first-order monotone boolean function has a p-level of (∞, ∞) if and only if it
is sequential
Proof. (⇒) It is sufficient to show that if cc(f ) = ∞, then f is sequential. Let us first prove the
following auxiliary result: given f : B k+1 → B a monotone function and f ′ : B k → B defined by
f ′ (x1 , . . . , xk ) = f (x1 , . . . , y, . . . , xk )
for some fixed y as the ith argument of f . Then cc(f ′ ) ≥ cc(f ).
Consider the two cases:
1. (cc(f ) = ∞) In this case, there is no linearly coherent subset of π1 (tr(f )), and hence there
can be no linearly coherent subset of π1 (tr(f ′ )) (otherwise, it would yield a linearly coherent
subset of π1 (tr(f )). Hence, cc(f ′ ) = ∞ ≥ cc(f ) by definition.
2. (cc(f ) < ∞) Given A ⊆ π1 (tr(f ′ )) a coherent subset of size cc(f ′ ). Let B be the following
set:
{(x1 , . . . , xk+1 ) ∈ π1 (tr(f )) : (x1 , . . . , xi−1 , xi+1 , . . . , xk+1 ) ∈ A, xi ≤ y} .
We check that B ⊆ π1 (tr(f )) is linearly coherent. First, notice that |B| = |A|. Moreover, we
see that for all tuples in B, the ith position is either a ⊥ or a value y. Added to the fact that A
is linearly coherent, we see that B must be linearly coherent, and hence cc(f ) ≤ cc(f ′ ).

11

And this proves the auxiliary result.
We now prove the sufficient condition by induction on the arity of f .
(base case) f : B → B. Consider f (⊥). If f (⊥) 6= ⊥, then by monotonicity f is constant, and
hence sequential. if f (⊥) = ⊥, then consider f (y) for a fixed y. This must be a constant, so f is
sequential (by the definition of sequentiality).
(induction step) Assume the result holds for all functions of arity k. Consider f : B k+1 → B,
with cc(f ) = ∞.
1. We first need to show that there exists an index of sequentiality. Assume not: for all i, for any
fixed xj , ∀j 6= i, f (x1 , . . . , ⊥, . . . , xk+1 ) 6= ⊥. Then π1 (tr(f )) must be ⊥-covering, which
contradicts cc(f ) = ∞.
2. Given i the index of sequentiality of f , look at the function f ′ (z1 , . . . , zk ) = f (z1 , . . . , y, . . . , zk )
for a fixed y in position i. By the auxiliary result, cc(f ′ ) = ∞, and the induction hypothesis
applies to show that f ′ and therefore f must be sequential.
⊔
⊓
(⇐) Immediate, since f sequential implies that f is PCF-definable, and hence f must be invariant under all sequentiality relations — including presequentiality relations.

5 Structural results
In this section, we use p-levels to guide our exploration of the CONT semilattice. The approach is
roughly as follows: we identify interesting classes of functions (stable functions, unstable functions,
stable-dominating functions, monovalued functions), and show that they have a natural characterization in terms of p-levels. We then use the p-level characterization to look for interesting natural
hierarchies. A hierarchy is deemed natural if it is made up of functions living on different p-levels.
We also show that interesting well-known functions also have a natural characterization in terms of
p-levels.

5.1 The STABLE semilattice
Define a stable degree of parallelism to be a degree of parallelism containing at least one stable
function. We can characterize stable degrees in terms of p-levels:
Proposition 5.1 A degree of parallelism is stable if and only if its p-level is of the form (i, j) with
i ≥ 2 and j ≥ 2
Proof. (⇒) Given f a stable function. Then cc(f ) ≥ 3,and by Lemma 4.2, f must have a p-level
of the form (i, j) with j ≥ cc(f ) − 1 ≥ 2. Since f is monotone, i ≥ 2.
(⇐) Given f with a p-level (i, j) with j ≥ 2. By Lemma 4.2, cc(f ) − 1 ≥ 2, so that cc(f ) ≥ 3.
Hence, f must be stable.
⊔
⊓
As a consequence, every function in a stable degree of parallelism must be stable. Let STABLE
be the subposet of CONT consisting of all stable degrees of parallelism.
Proposition 5.2 STABLE is a subsemilattice of CONT.

12

Proof. It is easy to see that the least upperbound of two stable degrees of parallelism is itself a stable
degree of parallelism. The degree of sequential functions is the bottom element of the semilattice
and the Berry-Plotkin function (BP) is its top element, as noted by Plotkin and reported by Curien
in [6].
⊔
⊓
The Berry-Plotkin function is defined by the following trace:
⊥
tt
ff

tt
ff
⊥

ff
⊥
tt

tt
ff
ff

We can in fact completely characterize the degree of parallelism of BP via presequentiality
levels:
Proposition 5.3 Given f a first-order monotone boolean function. Then f has a p-level of (2, 2) iff
f ≡ BP.
Proof. (⇒) Given f with a p-level of (2, 2). This means that bcc(f ) = 3, in other words, there
exists an A ⊆ π1 (tr(f )) bivalued and linearly coherent, with |A| = 3. We can assume without loss
of generality that one element of A returns tt and the remaining two return ff (otherwise, consider
neg(f ) which is equiparallel to f and has the desired property). Define g : tr(BP) → tr(f ) by
sending the first trace element of BP (the one returning tt) to the element of A returning tt, and the
remaining elements of BP to the elements of A returning ff. Since A is linearly coherent, it is clear
that g satisfies the condition of Proposition 2.2, and BP  f , Hence by Proposition 5.1, f is stable,
so f  BP.
(⇐) Given f ≡ BP. Then f must be invariant under the same sequentiality relations, hence the
p-level of f is the same as the p-level of BP, namely (2, 2).
⊔
⊓

5.2 The Gustave hierarchy
The structure of STABLE is non-trivial. Since the functions BUCC(n,m) are easily seen to be stable,
the whole Bucciarelli hierarchy is in STABLE. We can identify a subhierarchy of the Bucciarelli
hierarchy derived from the Gustave function [1]. The Gustave function GUST is given by the
following trace (in matrix form):
⊥
tt
ff

tt
ff
⊥

ff
⊥
tt

tt
tt
tt

Definition 5.4 Let GUSTi : B 2i+1 → B (i ≥ 1) be defined by the following trace (in matrix form):
⊥
ff
tt

tt
⊥
ff
..
.

ff
tt
⊥

···
···
···

tt
ff
tt

ff
tt
ff

tt
tt
tt
..
.

ff
tt

tt
ff

ff
tt

···
···

⊥
ff

tt
⊥

tt
tt

13

Note that GUST1 is just GUST. It is easy to verify the following:
Proposition 5.5 GUSTi ≡ BUCC(2i+1,2i+1) .
Proof. First note that a monovalued first-order monotone boolean function with |tr(f )| = cc(f ) =
n is such that f ≡ BUCC(n,n) , by an application of Proposition 2.2, and note that |tr(GUSTi )| =
cc(GUSTi ) = 2i + 1.
⊔
⊓
By Lemma 4.2, the functions GUSTi have a p-level of (∞, 2i). This characterization allows us
to derive the following result:
Proposition 5.6 There is no minimal stable non-sequential function.
Proof. Assume g is a stable non-sequential function that is minimal, i.e. for all f , f stable,
non-sequential, g  f .
Since g is not sequential, by Proposition 4.4, there must be some A, B, n such that g is not
invariant under SnA,B .
Consider GUST|A| . By the p-level of GUSTi functions, since |A| ≤ 2 |A|, GUST|A| is invariant under SnA,B .
Hence g 6 GUST|A| , a contradiction.
⊔
⊓
On the other hand, we can show that the Gustave hierarchy is co-final in the non-sequential
functions, that is any non-sequential function must dominate one of the functions in the hierarchy.
Proposition 5.7 Given f a stable non-sequential first-order monotone boolean function. Then there
exists an integer i such that GUSTi  f .
Proof. The function f being non-sequential implies that cc(f ) < ∞ by Propositions 4.4 and 4.2.
Moreover, f being stable implies that cc(f ) ≥ 3 (by Lemma 4.2 and Proposition 5.1). Let A be a linearly coherent subset of π1 (tr(f )) of size cc(f ). Define a arbitrary function g : tr(GUSTcc(f ) ) →
tr(f ) with π1 (g(tr(GUSTcc(f ) ))) = A. It is easy to see that the conditions of Proposition 2.2 are
satisfied, so that GUSTcc(f )  f .
⊔
⊓
Note that Propositions 5.6 and 5.7 can be derived directly from Bucciarelli’s result. We merely
identify a natural subset of the Bucciarelli hierarchy that is sufficient for our purpose.

5.3 The Bivalued-Gustave hierarchy
Functions in the Gustave hierarchy (and indeed, in the Bucciarelli hierarchy) are all monovalued.
We return to monovalued functions in Section 5.6. For now, let us extend the Gustave hierarchy to
a hierarchy of bivalued functions, the Bivalued-Gustave hierarchy.
Definition 5.8 Let BGUSTji : B 2i+1 → B (j ≤ i) be the function defined by the following trace
(in matrix form):
⊥
ff
tt

tt
⊥
ff
..
.

ff
tt
⊥

···
···
···

tt
ff
tt

ff
tt
ff

r1
r2
r3
..
.

ff
tt

tt
ff

ff
tt

···
···

⊥
ff

tt
⊥

r2i
r2i+1

14

with
rl =

(

ff if 1 ≤ l ≤ j
tt otherwise

Let us first show that the j parameter in BGUSTji is unnecessary: we may pick BGUST1i as a
representative of the class of BGUSTji functions, and drop the superscript to refer to the function
as BGUSTi .
′

Lemma 5.9 Given j, j ′ ≤ i, BGUSTji ≡ BGUSTji .
Proof. We prove by induction on j that for all j,BGUSTji ≡ BGUST1i . The case j = 1 is trivial.
For the induction step (j ≥ 2), assume that BGUSTij−1 ≡ BGUST1i and consider BGUSTji . We
show BGUSTji ≡ BGUSTij−1 . Define the following terms:
M1 = λf λx1 . . . x2i+1 .if f (x1 , . . . , x2i+1 )
then f (x2 , . . . , x2i+1 , x1 ) else ff fi
M2 = λf λx1 . . . x2i+1 .if f (x1 , . . . , x2i+1 )
then tt else f (x2i+1 , x1 , . . . , x2i ) fi
It is not hard to see that BGUSTji = M1 BGUSTij−1 and BGUSTij−1 = M2 BGUSTji ,
thereby showing BGUSTji ≡ BGUSTij−1 ≡ BGUST1i by the induction hypothesis.
⊔
⊓
It remains to show that the functions BGUSTi actually form a hierarchy. First note that by
Lemma 4.2 BGUSTi has a p-level of (2i, 2i).
Proposition 5.10 BGUSTi  BGUSTj iff i ≥ j.
Proof. (⇐) A straightforward application of Proposition 2.2: consider any surjective function
g : tr(BGUSTi ) → tr(BGUSTj ) sending the unique trace element returning tt to the unique trace
element returning tt, and any trace element returning ff to any trace element returning ff. It is easy
to see that all conditions of Proposition 2.2 are satisfied, and BGUSTi  BGUSTj .
(⇒) Assume i < j. The p-level of BGUSTi is (2i, 2i) and the p-level of BGUSTj is (2j, 2j).
By Corollary 4.1, BGUSTi 6 BGUSTj .
⊔
⊓
The following result is immediate:
Proposition 5.11 For all i, GUSTi  BGUSTi .
⊔
⊓

Proof. Via Proposition 2.2.

Combining functions in the Gustave hierarchy and the Bivalued-Gustave hierarchy via the least
upperbound operation produces a two-dimensional hierarchy, with functions of the form BGUSTi +
GUSTj . A trivial application of Lemma 4.3 gives a p-level of (2i, 2 min(i, j)) for BGUSTi +
GUSTj . This allows us to derive the following governing equations describing the structure of the
hierarchy:
Proposition 5.12 BGUSTi + GUSTj  BGUSTi′ + GUSTj ′ iff i′ ≤ i and min(i′ , j ′ ) ≤
min(i, j).
15

Proof. (⇒) We prove the contrapositive. If i < i′ or min(i, j) < min(i′ , j ′ ), then by Corollary 4.1
and the p-level of functions in the hierarchy, BGUSTi + GUSTj 6 BGUSTi′ + GUSTj ′ .
(⇐) Since i′ ≤ i, Proposition 5.10 tells us that BGUSTi ≤ BGUSTi′ ≤ BGUSTi′ + GUSTj ′ .
We then consider three cases:
1. (min(i, j) = i) Proposition 5.11 implies that
GUSTj  BGUSTj  BGUSTi  BGUSTi′ + GUSTj ′
Hence, BGUSTi + GUSTj  BGUSTi′ + GUSTj ′ .
2. (min(i, j) = j, min(i′ , j ′ ) = i′ ) By assumption, i′ ≤ j, and hence by Proposition 5.11,
GUSTj  BGUSTj  BGUSTi′  BGUSTi′ + GUSTj ′ . Hence BGUSTi + GUSTj 
BGUSTi′ + GUSTj ′ .
3. (min(i, j) = j, min(i′ , j ′ ) = j ′ ) By assumption, j ′ ≤ j, and hence
GUSTj  GUSTj ′  BGUSTi′ + GUSTj ′
Hence BGUSTi + GUSTj  BGUSTi′ + GUSTj ′ .

⊔
⊓

5.4 The UNSTABLE semilattice
Define an unstable degree of parallelism to be a degree of parallelism containing no stable function.
It is easy to show that a degree of parallelism is unstable if and only if it has a p-level of the form
(i, 1) with i ≥ 2, by Proposition 5.1. Let UNSTABLE be the subposet of CONT consisting of all
unstable degrees of parallelism. Define the Detector function (DET) to simply return tt if one of
its two inputs has a value (tt or ff indifferently). For various reasons, it is simpler to work with the
following function ttDET which is easily seem to be equiparallel to DET:
tt
⊥

⊥
tt

tt
tt

Proposition 5.13 UNSTABLE is a subsemilattice of CONT.
Proof. It is easy to see that the least upperbound of two unstable degrees of parallelism is unstable.
The top element of UNSTABLE is the degree of POR and its bottom element is the degree of the
Detector function. This last fact is an application of Proposition 2.2: given f an unstable first-order
monotone boolean function; since f is unstable, there must exist A ⊆ π1 (tr(f )) with A coherent
and |A| = 2. Define a function
g : tr(ttDET) → tr(f )
with the only constraint that each element of the trace of ttDET goes to a distinct element of the
trace of f corresponding to the subset A. It is easy to see that all the conditions of Proposition 2.2
are met, hence ttDET  f .
⊔
⊓
Detector first appeared in the context of asynchronous dataflow networks. Rabinovich shows in
[12] that DET is minimal among unstable functions in that context.
16

A degree of parallelism is unstable if and only if it is not stable, so we see that the STABLE and
the UNSTABLE semilattices form a partition of the full CONT semilattice. We presently identify
one hierarchy of functions in UNSTABLE (another will be presented in Section 5.5 ); functions in
this hierarchy are derived from POR:
Definition 5.14 Let PORi : B i → B (i ≥ 2) be defined by the following trace (in matrix form):
tt
tt

tt
tt
..
.

tt
tt

···
···

tt
⊥

⊥
tt

tt
tt
..
.

tt
tt
⊥
ff

tt
⊥
tt
ff

⊥
tt
tt
ff

···
···
···
···

tt
tt
tt
ff

tt
tt
tt
ff

tt
tt
tt
ff

Note that POR2 is just POR. PORi takes i inputs and returns tt if at least i − 1 are tt, and ff if
all are ff. These functions span the whole range of allowable p-levels for unstable functions as the
next proposition shows:
Proposition 5.15 PORi has a p-level of (i, 1).
Proof. Since PORi is monotone and unstable, it must have a p-level of the form (j, 1) for some
j ≥ 2, by the characterization of p-levels of monotone and stable functions.
By inspection, we see that the only bivalued coherent subset of π1 (tr(PORi )) is π1 (tr(PORi ))
itself. Hence, bcc(f ) = i + 1 and by Lemma 4.2, j = bcc(f ) − 1 = i.
⊔
⊓
These functions indeed form a hierarchy:
Proposition 5.16 PORi  PORj iff i ≥ j.
Proof. (⇐) Consider the following PCF-term:
M = λf.λx1 . . . xi+1 .ALLEQ(t1 (x1 , . . . , xi+1 ), . . . , ti+1 (x1 , . . . , xi+1 ))
where
ALLEQ = λx1 . . . xi+1 .if (x1 = . . . = xi+1 ) then x1 else ⊥ fi
which returns the value v if and only if all the arguments have the value v.
Each !
tj is an application of PORi to a subset of i inputs out of the i + 1 possible inputs. Since
i+1
= i + 1, there are i + 1 such terms. We claim this term is such that PORi+1 =
i
M PORi .
1. The tj functions all return tt iff at least i tt’s appear in their arguments
(a) (at least i tt’s) Each subset of size i has at least i + 1 tt’s, so each tj function returns tt.
(b) (less then i tt’s) There exists one subset of size i with less than i − 1 tt’s, so the corresponding tj function returns ⊥.
17

2. The tj functions all return ff iff all inputs are ff.
(a) (all ff’s) Every tj returns ff.
(b) (not all ff’s) There exists a subset of size i with not all inputs being ff. The corresponding
tj does not return ff.
(⇒) Assume i < j. The result is immediate by Corollary 4.1 and Proposition 5.15.

5.5 The SDOM semilattice
It is clear that unstable functions are strictly more powerful than stable functions, in the sense that
no stable function can implement an unstable function, but unstable functions can implement stable
functions. In this section, we characterize the unstable functions that can implement all stable
functions, and show that they form a subsemilattice of UNSTABLE.
Definition 5.17 Let f be an unstable first-order monotone boolean function. We say f is stabledominating if for any stable first-order monotone boolean function g, we have g  f .
Since the STABLE semilattice has a top element BP, a necessary and sufficient condition for
an unstable function f to be stable-dominating is to have BP  f . Since any stable-dominating
function must also dominate DET (the bottom element of UNSTABLE), we have that f is stabledominating if and only if BP + DET  f . This allows us to derive the following characterization
of stable-dominating functions:
Proposition 5.18 Given f an unstable first-order monotone boolean function. Then f is stabledominating iff f has a p-level of (2, 1).
Proof. (⇒) Assume f is stable-dominating. Then by previous argument, BP + DET  f . Since
BP has p-level (2, 2) and DET has p-level (∞, 1), BP + DET has p-level (2, 1) by Lemma 4.3.
Assume f does not have a p-level of (2, 1). By Proposition 4.4, f must have a p-level of (i, j) with
i ≥ 2, j ≥ 1 and i 6= 2 or j 6= 1. But by Corollary 4.1, we get that BP + DET 6 f , a contradiction.
(⇐) Given f with p-level (2, 1). By the characterization of the p-level of stable functions, f
is unstable. We need only check that BP  f . By Lemma 4.2, bcc(f ) = 3. Let A be the subset
of π1 (tr(f )) of size 3. Assume without loss of generality that A has one element returning tt and
two elements returning ff (if not, consider neg(f ) which is equiparallel to f ). Define a function
g : tr(BP) → tr(f ) sending the element of the trace of BP returning tt to the element of A
returning tt and the elements of the trace of BP returning ff to the elements of A returning ff. It is
easy to see that all the conditions of Proposition 2.2 hold, and hence we have BP  f . So f is
stable-dominating.
⊔
⊓
Define a stable-dominating degree of parallelism to be a degree of parallelism containing a
stable-dominating function. By Proposition 5.18, every function in a stable-dominating degree of
parallelism is stable-dominating. Let SDOM be the subposet of CONT (in fact, of UNSTABLE)
consisting of all stable-dominating degrees of parallelism.
Proposition 5.19 SDOM is a subsemilattice of UNSTABLE.

18

Proof. It is easy to see by the above characterization that the least upperbound of two stabledominating degrees of parallelism is itself stable-dominating. The bottom element of SDOM is the
degree of BP + DET, and its top element is the degree of POR.
⊔
⊓
To show this subsemilattice is non-trivial, we exhibit an hierarchy of functions in SDOM. Note
however that because stable-dominating functions are all in the same p-level, we cannot show inexpressibility using presequentiality relations. Consider the functions BP + PORi , which are easily
seen to be stable-dominating. Note that BP + POR2 ≡ POR2 ≡ POR. These functions form a
hierarchy:
Proposition 5.20 BP + PORi  BP + PORj iff i ≥ j.
Proof. (⇐) We know BP  BP + PORj for all j ≥ 2. Similarly, by Proposition 5.16, PORi 
PORj  BP + PORj . Hence, by the property of least upperbounds, we get that BP + PORi 
BP + PORj .
(⇒) Assume i < j. Define the following sequentiality relation of arity j
{1,2},{1,2}

R = Sj

{1,...,j},{1,...,j}

∩ · · · ∩ Sj

By Proposition 3.2, it is sufficient to show that BP + PORj is invariant under R, but BP + PORi
is not.
1. (BP + PORj invariant) Going back to the definition of +, without loss of generality we can
take
(BP + PORj )(tt, x1 , . . . , xj ) = PORj (x1 , . . . , xj )
For the sake of
assume
BP + PORj is not invariant under R. Then there


 contradiction,
k
1
1
exists tuples x1 , . . . , xj , · · · , x1 , . . . , xkj ∈ R . Let y = (y1 , . . . , yj ), with ym =
BP + PORj (x1m , . . . , xkm ), and y 6∈ R.

{1,...,m},{1,...,m}

By induction on 2 ≤ m ≤ j, we show BP + PORj must be invariant under Sj
For m = 2, BP+PORj is invariant under
4.4.

{1,2},{1,2}
Sj

.

by the Closure Lemma and Proposition

For the induction step, assume for the sake of contradiction that BP + PORj is not invariant
{1,...,m+1},{1,...,m+1}
under Sj
. Then there is no ⊥ in y1 , . . . , ym+1 , and there exists I, J with
{1,...,m},{1,...,m}

yI 6= yJ . By the induction hypothesis, BP + PORj is invariant under Sj
, so
we must have y1 = · · · = ym , and hence the only possibility is that ym+1 6= y1 . Since no ⊥
appears in the resulting tuple, the first tuple above must all be tt or all be ff, by the definition
of +. If it is all ff, then the columns of the tuples must come from the trace of BP, but since
the first m columns are linearly coherent and return the same result, this would mean that
the Egli-Milner lowerbound of the first m column has only one element, and since it is also
coherent with the last column (which returns a different result), this contradicts BP being
stable. Hence, the first tuple must be all tt, and the columns must come from the trace of
PORj . But the m + 1 columns form a linearly coherent set of size less than or equal to j, and
we can easily show that they cannot contain the trace element of PORj that returns false. So
we must have ym+1 = y1 .
{1,...,m},{1,...,m}

Therefore, BP+PORj is invariant under Sj
is invariant under R.

19

for 2 ≤ m ≤ j, hence BP+PORj

2. (BP + PORi not invariant) Again without loss of generality, we can take
(BP + PORi )(tt, x1 , . . . , xi ) = PORi (x1 , . . . , xi )
{1,...,i+1},{1,...,i+1}

We show that BP + PORi is not invariant under Sj
variant under R. Consider the following tuples of length j:




, implying it is not in-



(tt . . . , tt) , x11 , . . . , x1i+1 , ⊥, . . . , ⊥ , · · · , xi1 , . . . , xii+1 , ⊥, . . . , ⊥



where {(tt, x1m , . . . , xim )} (m ≤ i + 1) is the subset of the first projection of the trace of BP +
{1,...,i+1},{1,...,i+1}
PORi corresponding to PORi . It is easy to see that all those tuples are in Sj
.
Applying BP + PORi to the columns of the tuples yields the tuple (tt, . . . , tt, ff, ⊥, . . . , ⊥),
| {z }
i

which is not in

{1,...,i+1},{1,...,i+1}
Sj
.

⊔
⊓

5.6 The MONO semilattice
Up to this point all the semilattices we have introduced were related in some way to the partitioning
of functions according to whether or not they were stable. We now consider a different characteristic
and derive a corresponding semilattice. Define a monovalued degree of parallelism to be a degree of
parallelism containing at least one monovalued function. We can characterize monovalued degrees
of parallelism by their p-level:
Proposition 5.21 A degree of parallelism is monovalued if and only if its p-level is of the form
(∞, j) with j ≥ 1.
Proof. If f is monovalued then bcc(f ) = ∞, since there can be no bivalued coherent subset of
π1 (tr(f )). Moreover, since f is monotone, it must have a p-level of the form (i, j) with i ≥ 2 and
j ≥ 1. We know i = ∞ (since bcc(f ) = ∞), so f must have a p-level of the form (∞, j) with
j ≥ 1.
⊔
⊓
Let MONO be the subposet of CONT containing all monovalued degrees of parallelism.
Proposition 5.22 MONO is a subsemilattice of CONT.
Proof. The least upperbound of two monovalued degrees of parallelism is itself monovalued. The
bottom element of MONO is the degree of all sequential functions, and its top element is the degree
of DET, the Detector function. To show this, consider f a monovalued first-order monotone boolean
function. Without loss of generality, assume f always returns tt (if not, consider neg(f ) which is
equiparallel to f ). Let ttDETn be the function of arity n that returns tt if one of its arguments is tt.
It is not hard to show that for all n, ttDETn  ttDET. Let n = |tr(f )|. Consider the following
PCF-term:
M = λpλx1 . . . xk .p(t1 (x1 , . . . , xk ), . . . , tn (x1 , . . . , xk ))
where tj is a term checking if its arguments agree with the jth element of π1 (tr(f )) — and returning
tt if they do and blocking if they don’t. For example, for the Gustave function GUST, the terms
20

look like:
t1 = λx1 x2 x3 .(x2 ∧ ¬x3 )
t2 = λx1 x2 x3 .(x1 ∧ ¬x2 )
t3 = λx1 x2 x3 .(x3 ∧ ¬x1 )
It is easy to see that f = M ttDETn , and since ttDETn  ttDET, f  ttDET.

⊔
⊓

We note that the MONO semilattice contains the Bucciarelli hierarchy.
We can fully characterize the degree of parallelism of DET via p-levels, as we did with BP:
Proposition 5.23 Given f a first-order monotone boolean function. Then f has a p-level of (∞, 1)
iff f ≡ DET.
Proof. (⇒) If f has a p-level of (∞, 1), then f must be both monovalued and unstable. By
minimality of DET in the UNSTABLE semilattice, DET  f . Since DET is the top element for
monovalued functions and f monovalued, f  DET. Hence f ≡ DET.
(⇐) Given f ≡ DET. Then f must be invariant under the same sequentiality relations, hence
the p-level of f is the same as the p-level of DET, namely (∞, 1).
⊔
⊓
Since a function is unstable if and only if its p-level is (i, 1) for some i ≥ 2, and it is monovalued
if and only if its p-level is (∞, j) for some j ≥ 1, [DET] is the only unstable and monovalued degree
of parallelism.
We will mention a final interesting result concerning monovalued degrees of parallelism. We
can further characterize monovalued degrees of parallelism, a notion involving the description of a
function, via extensional properties of the corresponding functions. A function f is subsequential
if there exists a sequential function g that extends f , that is that dominates f in the extensional
ordering on B k .
Proposition 5.24 A function f is subsequential if and only if [f ] is monovalued.
Proof. The proof is a corollary of the proposition in [5] which in our terminology states that
given f a first-order monotone boolean function, then f is subsequential iff bcc(f ) = ∞. By this
proposition, f is subsequential iff bcc(f ) = ∞. By Lemma 4.2, f is subsequential iff f has p-level
(∞, j) for some j ≥ 1. By Proposition 5.21, f is subsequential iff [f ] is monovalued.
⊔
⊓
Therefore, every subsequential function is expressible by DET and conversely, DET can only
express subsequential functions.

6 Conclusion
In this paper, we set out to explore the structure of CONT, the semilattice of degrees of parallelism
of first-order monotone boolean functions. It is known that Sieber’s sequentiality relations fully
characterize the ordering on the semilattice. By turning our attention to presequentiality relations,
a simple class of sequentiality relations, we were able to focus on the skeleton of the definability
preorder. The advantage of looking at presequentiality relations is that we were able to completely
characterize the set of presequentiality relations under which a given function is invariant via their
p-level, a pair of integers which can be extracted from the trace of the function.
21

We showed that interesting classes of functions have natural characterizations in terms of plevels, namely stable functions, unstable functions, stable-dominating functions and monovalued
functions, and moreover exhibited natural hierarchies within those classes of functions, hierarchies
that make up the skeleton of the definability preorder. We were also able to completely charaterize
various well-known functions in terms of p-levels: any function with a p-level of (2, 2) is equiparallel to BP, any function with a p-level of (∞, 1) is equiparallel to DET, any function with a p-level
of (2, 1) is equiparallel to POR.
The keys to the p-level characterization are clearly the Reduction and Closure Lemmas, which
allow us to derive canonical representatives for large classes of presequentiality relations. The characterization itself is based on the fact that only two canonical presequentiality relations are needed
to describe the full set of presequentiality relations under which a function is invariant. The next
obvious step in the investigation is to extend this result to full sequentiality realtions. The question becomes: can we find canonical representatives of classes of sequentiality relations? A look
at more complicated examples of sequentiality relations (for example, the ones used in the proof
in [2], or in the proof of the strictness of the BP + PORi hierarchy in Proposition 5.20) indicates
that canonical representatives for full sequentiality relations are far less nicely characterized than
their presequentiality counterparts. This is an area of future work, along the lines of the hypergraph
approach of [2, 5]. Another area of future work is a study of unstable functions (or unstable degrees
of parallelism). The structure of p-levels for stable functions is richer than for unstable functions.
Moreover, Bucciarelli’s original hierarchy fully lives in the STABLE semilattice. It would be interesting to see if the structure of the UNSTABLE semilattice is equivalently complicated, or simpler
in some respect.
Acknowledgments. Thanks to the anonymous referees for suggestions that helped improve and
tighten the presentation, and for various technical corrections.

References
[1] G. Berry. Bottom-up computations of recursive programs. RAIRO Informatique Théorique,
10(3):47–82, 1976.
[2] A. Bucciarelli. Degrees of parallelism in the continuous type hierarchy. Theoretical Computer
Science, 177(1):59–71, 1997.
[3] A. Bucciarelli and T. Erhard. Sequentiality and strong stability. In Sixth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1991.
[4] A. Bucciarelli and T. Erhard. Sequentiality in an extensional framework. Information and
Computation, 110(2), 1994.
[5] A. Bucciarelli and P. Malacaria. Relative definability of boolean functions via hypergraphs. In
12th International Workshop on Mathematical Foundations of Programming Semantics, 1997.
[6] P-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming.
Birkhäuser, revised edition, 1993.
[7] B. Lichtenthäler. Degrees of parallelism. Master’s thesis, Universität - GH Siegen, 1996.
Appears as Informatik Berichte 96-01.
22

[8] R. Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science,
4:1–22, 1977.
[9] G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science,
5:223–256, 1977.
[10] G. D. Plotkin. Lambda-definability in the full type hierarchy. In J. Hindley J. Seldin, editor, To
H.B.Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 363–374.
Academic Press, 1980.
[11] R. Pucella. Investigations on relative definability in PCF. Master’s thesis, McGill University,
1996.
[12] A. Rabinovich. Modularity and expressibility for nets of relations.
35(4):203–327, 1998.

Acta Informatica,

[13] V. Y. Sazonov. Degrees of parallelism in computations. In Proceedings of the Conference
on Mathematical Foundations of Computer Science, volume 45 of Lecture Notes in Computer
Science, 1976.
[14] K. Sieber. Reasoning about sequential functions via logical relations. In P. Johnstone M. Fourman and A. Pitts, editors, Proceedings of the LMS Conference on the Applications of Categories to Computer Science. Cambridge University Press, 1992.
[15] A. Stoughton. Mechanizing logical relations. In Proceedings of the Ninth International Conference on Mathematical Foundations of Programming Semantics, volume 802 of Lecture
Notes in Computer Science. Springer-Verlag, 1994.
[16] M. B. Trakhtenbrot. On interpreted functions in program schemes. In Sistemnoe i teoretic̃eskoe
programmirovanie, pages 188–211. Novosibirsk, 1973. (in Russian).
[17] M. B. Trakhtenbrot. On representation of sequential and parallel functions. In Proceedings of
the Fourth Symp. on Mathematical Foundations of Computer Science, volume 32 of Lecture
Notes in Computer Science. Springer, 1975.

23

