Set-based Operators and Fixed-Points by Support

Andreas Abel

April 22, 2004

In Abel and Altenkirch’s article A Predicative Analysis of Structural Recursion [AA02] one finds on page 34 a definition of the semantics [[σ]] of a strictly positive inductive type σ. This definition (5.1) is itself a strictly-positive inductive definition on the meta-level. In the following we exhibit its correspondence to the algorithmic construction of a least fixed-point as found in Pierce’s book Types and Programming Languages [Pie02] on pages 290–295.

First we give a simplified version of the definition restricted to a single type variable.

Definition 5.1. For σ ∈ Ty(X) and a closed type τ let

[[σ]] : P (Val^{τ}) → P (Val^{σ(τ)})

be a monotone operator with a urelement relation

U^{σ} ⊆ Val^{τ} × Val^{σ(τ)}

such that for all v ∈ Val^{σ(τ)} and u ∈ Val^{τ}:

v ∈ [[σ]](V)  u U^{σ} v ; \overline{(sb1)} ; u ∈ V  v ∈ [[σ]](Val^{τ}) ; \overline{(sb2)} ; v ∈ [[σ]](U^{σ}(v))

where U^{σ}(v) = {w | w U^{σ}v}. The interpretation of μ-types is then obtained by

{v ∈ [[σ]](Val^{μX.σ}) ∀u. u U^{σ} v → u ∈ [[μX.σ]] \atop fold(v) ∈ [[μX.σ]]}

Pierce (page 290) assumes a universe U and an operator F : P(U) → P(U) and calls a set X generating for x if x ∈ F (X). The support support_{F} (x) of x is the least generating set for x if there exists one, otherwise undefined. Consider the following correspondences:

Abel, Altenkirch  Pierce
Val  U
[[σ]]  F
U^{σ}  support_{F}

Then (sb2) expresses that U^{σ}(v) is a generating set for v if v is [[σ]]-generateable. Property (sb1) can be rewritten as if v ∈ [[σ]](V) then U^{σ} (v) ⊆ V, expressing the second condition on the support of v that it is the least generating set for v. Hence, for [[σ]]-generateable elements v, it holds that U^{σ}(v) = support_{[[σ]]}(v).

Extending the urelement relation to sets,

U^{σ}(V) = ⋃_{v∈V} U^{σ}(v),

property (sb1) becomes W ⊆ [[σ]](V) implies U^{σ}(W) ⊆ V, exhibiting a Galois connection. This corresponds to Pierce’s Lemma 21.5.7 (page 293). Finally, in Exercise 21.5.13 Pierce gives a partial algorithm to test whether a set X is contained in the least-fixed point μF. The logical reading of the algorithm is

X ⊆ μF iff X empty or (support_{F} (X) defined and support_{F} (X) ⊆ μF)

Abel and Altenkirch’s rule for introducing elements of an inductive type, generalized to sets reads

{V ⊆ [[σ]](Val^{μX.σ}) U^{σ}(V) ⊆ [[μX.σ]] \atop fold V ⊆ [[μX.σ]]}.

The first condition states that all elements of V are [[σ]]-generateable which means that the support of V is defined. Modulo the folding operation, which comes from iso-recursive types, the rule now exactly expresses Pierce’s algorithm.

References

[AA02] Andreas Abel and Thorsten Altenkirch. A predicative analysis of structural recursion. Journal of Functional Programming, 12(1):1–41, January 2002.

[Pie02] Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.