5.3 W-types


Inductive types are very general, which is excellent for their usefulness and applicability, but makes them difficult to study as a whole. Fortunately, they can all be formally reduced to a few special cases. It is beyond the scope of this book to discuss this reductionPlanetmathPlanetmath β€” which is anyway irrelevant to the mathematician using type theoryPlanetmathPlanetmath in practice β€” but we will take a little time to discuss the one of the basic special cases that we have not yet met. These are Martin-LΓΆf’s W-types, also known as the types of well-founded trees. 𝖢-types are a generalizationPlanetmathPlanetmath of such types as natural numbersMathworldPlanetmath, lists, and binary treesMathworldPlanetmath, which are sufficiently general to encapsulate the β€œrecursion” aspect of any inductive type.

A particular 𝖢-type is specified by giving two parameters A:𝒰 and B:A→𝒰, in which case the resulting 𝖢-type is written 𝖢(a:A)⁒B⁒(a). The type A represents the type of labels for 𝖢(a:A)⁒B⁒(a), which function as constructors (however, we reserve that word for the actual functions which arise in inductive definitions). For instance, when defining natural numbers as a 𝖢-type, the type A would be the type 𝟐 inhabited by the two elements 0𝟐 and 1𝟐, since there are precisely two ways to obtain a natural number β€” either it will be zero or a successorMathworldPlanetmathPlanetmathPlanetmath of another natural number.

The type family B:A→𝒰 is used to record the arity of labels: a label a:A will take a family of inductive arguments, indexed over B⁒(a). We can therefore think of the β€œB⁒(a)-many” arguments of a. These arguments are represented by a function f:B⁒(a)→𝖢(a:A)⁒B⁒(a), with the understanding that for any b:B⁒(a), f⁒(b) is the β€œb-th” argument to the label a. The 𝖢-type 𝖢(a:A)⁒B⁒(a) can thus be thought of as the type of well-founded trees, where nodes are labeled by elements of A and each node labeled by a:A has B⁒(a)-many branches.

In the case of natural numbers, the label 0𝟐 has arity 0, since it constructs the constant zero; the label 1𝟐 has arity 1, since it constructs the successor of its argument. We can capture this by using simple elimination on 𝟐 to define a function π—‹π–Ύπ–ΌπŸβ’(𝒰,𝟎,𝟏) into a universePlanetmathPlanetmath of types; this function returns the empty type 𝟎 for 0𝟐 and the unit type 𝟏 for 1𝟐. We can thus define

𝐍𝐰:≑𝖢(b:𝟐)π—‹π–Ύπ–ΌπŸ(𝒰,𝟎,𝟏)

where the superscript 𝐰 serves to distinguish this version of natural numbers from the previously used one. Similarly, we can define the type of lists over A as a 𝖢-type with 𝟏+A many labels: one nullary label for the empty list, plus one unary label for each a:A, corresponding to appending a to the head of a list:

π–«π—‚π—Œπ—(A):≑𝖢(x:𝟏+A)π—‹π–Ύπ–ΌπŸ+A(𝒰, 0,Ξ»a. 1).

In general, the 𝖢-type 𝖢(x:A)⁒B⁒(x) specified by A:𝒰 and B:A→𝒰 is the inductive type generated by the following constructor:

  • β€’

    π—Œπ—Žπ—‰:∏(a:A)(B(a)→𝖢(x:A)B(x))→𝖢(x:A)B(x).

The constructor π—Œπ—Žπ—‰ (short for supremum) takes a label a:A and a function f:B⁒(a)→𝖢(x:A)⁒B⁒(x) representing the arguments to a, and constructs a new element of 𝖢(x:A)⁒B⁒(x). Using our previous encoding of natural numbers as 𝖢-types, we can for instance define

0𝐰:β‰‘π—Œπ—Žπ—‰(0𝟐,Ξ»x.π—‹π–Ύπ–ΌπŸŽ(𝐍𝐰,x)).

Put differently, we use the label 0𝟐 to construct 0𝐰. Then, π—‹π–Ύπ–ΌπŸβ’(𝒰,𝟎,𝟏,0𝟐) evaluates to 𝟎, as it should since 0𝟐 is a nullary label. Thus, we need to construct a function f:πŸŽβ†’ππ°, which represents the (zero) arguments supplied to 0𝟐. This is of course trivial, using simple elimination on 𝟎 as shown. Similarly, we can define

1𝐰 :β‰‘π—Œπ—Žπ—‰(1𝟐,Ξ»x. 0𝐰)
2𝐰 :β‰‘π—Œπ—Žπ—‰(1𝟐,Ξ»x. 1𝐰)

and so on.

We have the following inductionMathworldPlanetmath principle for 𝖢-types:

  • β€’

    When proving a statement E:(𝖢(x:A)⁒B⁒(x))→𝒰 about all elements of the 𝖢-type 𝖢(x:A)⁒B⁒(x), it suffices to prove it for π—Œπ—Žπ—‰β’(a,f), assuming it holds for all f⁒(b) with b:B⁒(a). In other words, it suffices to give a proof

    e:∏(a:A)∏(f:B(a)→𝖢(x:A)B(x))∏(g:∏(b:B(a))E(f(b)))E⁒(π—Œπ—Žπ—‰β’(a,f))

The variable g represents our inductive hypothesis, namely that all arguments of a satisfy E. To state this, we quantify over all elements of type B⁒(a), since each b:B⁒(a) corresponds to one argument f⁒(b) of a.

How would we define the function π–½π—ˆπ—Žπ–»π—…π–Ύ on natural numbers encoded as a 𝖢-type? We would like to use the recursion principle of 𝐍𝐰 with a codomain of 𝐍𝐰 itself. We thus need to construct a suitable function

e:∏(a:𝟐)∏(f:B(a)→𝐍𝐰)∏(g:B(a)→𝐍𝐰)𝐍𝐰

which will represent the recurrence for the π–½π—ˆπ—Žπ–»π—…π–Ύ function; for simplicity we denote the type family π—‹π–Ύπ–ΌπŸβ’(𝒰,𝟎,𝟏) by B.

Clearly, e will be a function taking a:𝟐 as its first argument. The next step is to perform case analysis on a and proceed based on whether it is 0𝟐 or 1𝟐. This suggests the following form

e:≑λa.π—‹π–Ύπ–ΌπŸ(C,e0,e1,a)

where

C:β‰‘βˆ(f:B(a)→𝐍𝐰)∏(g:B(a)→𝐍𝐰)𝐍𝐰

If a is 0𝟐, the type B⁒(a) becomes 𝟎. Thus, given f:πŸŽβ†’ππ° and g:πŸŽβ†’ππ°, we want to construct an element of 𝐍𝐰. Since the label 0𝟐 represents 𝟎, it needs zero inductive arguments and the variables f and g are irrelevant. We return 0𝐰 as a result:

e0:≑λf.Ξ»g. 0𝐰

Analogously, if a is 1𝟐, the type B⁒(a) becomes 𝟏. Since the label 1𝟐 represents the successor operator, it needs one inductive argument β€” the predecessor β€” which is represented by the variable f:πŸβ†’ππ°. The value of the recursive call on the predecessor is represented by the variable g:πŸβ†’ππ°. Thus, taking this value (namely g⁒(⋆)) and applying the successor operator twice thus yields the desired result:

e1:≑λf.Ξ»g.π—Œπ—Žπ—‰(1𝟐,(Ξ»x.π—Œπ—Žπ—‰(1𝟐,(Ξ»y.g(⋆))))).

Putting this together, we thus have

π–½π—ˆπ—Žπ–»π—…π–Ύ:≑𝗋𝖾𝖼𝐍𝐰(𝐍𝐰,e)

with e as defined above.

The associated computation rule for the function 𝗋𝖾𝖼𝖢(x:A)⁒B⁒(x)⁒(E,e):∏(w:𝖢(x:A)B(x))E⁒(w) is as follows.

  • β€’

    For any a:A and f:B⁒(a)→𝖢(x:A)⁒B⁒(x) we have

    𝗋𝖾𝖼𝖢(x:A)⁒B⁒(x)(E,e,π—Œπ—Žπ—‰(a,f))≑e(a,f,(Ξ»b.𝗋𝖾𝖼𝖢(x:A)⁒B⁒(x)(E,f(b)))).

In other words, the function 𝗋𝖾𝖼𝖢(x:A)⁒B⁒(x)⁒(E,e) satisfies the recurrence e.

By the above computation rule, the function π–½π—ˆπ—Žπ–»π—…π–Ύ behaves as expected:

π–½π—ˆπ—Žπ–»π—…π–Ύβ’(0𝐰) ≑𝗋𝖾𝖼𝐍𝐰(𝐍𝐰,e,π—Œπ—Žπ—‰(0𝟐,Ξ»x.π—‹π–Ύπ–ΌπŸŽ(𝐍𝐰,x)))
≑e(0𝟐,(Ξ»x.π—‹π–Ύπ–ΌπŸŽ(𝐍𝐰,x)),(Ξ»x.π–½π—ˆπ—Žπ–»π—…π–Ύ(π—‹π–Ύπ–ΌπŸŽ(𝐍𝐰,x))))
≑et((Ξ»x.π—‹π–Ύπ–ΌπŸŽ(𝐍𝐰,x)),(Ξ»x.π–½π—ˆπ—Žπ–»π—…π–Ύ(π—‹π–Ύπ–ΌπŸŽ(𝐍𝐰,x))))
≑0𝐰
and
π–½π—ˆπ—Žπ–»π—…π–Ύβ’(1𝐰) ≑𝗋𝖾𝖼𝐍𝐰⁒(𝐍𝐰,e,π—Œπ—Žπ—‰β’(1𝟐,λ⁒x⁒. 0𝐰))
≑e(1𝟐,(Ξ»x. 0𝐰),(Ξ»x.π–½π—ˆπ—Žπ–»π—…π–Ύ(0𝐰)))
≑ef((Ξ»x. 0𝐰),(Ξ»x.π–½π—ˆπ—Žπ–»π—…π–Ύ(0𝐰)))
β‰‘π—Œπ—Žπ—‰(1𝟐,(Ξ»x.π—Œπ—Žπ—‰(1𝟐,(Ξ»y.π–½π—ˆπ—Žπ–»π—…π–Ύ(0𝐰)))))
β‰‘π—Œπ—Žπ—‰(1𝟐,(Ξ»x.π—Œπ—Žπ—‰(1𝟐,(Ξ»y. 0𝐰))))
≑2𝐰

and so on.

Just as for natural numbers, we can prove a uniqueness theorem for 𝖢-types:

Theorem 5.3.1.

Let g,h:∏(w:W(x:A)B(x))E⁒(w) be two functions which satisfy the recurrence

e:∏a,f(∏b:B⁒(a)E⁒(f⁒(b)))β†’E⁒(π—Œπ—Žπ—‰β’(a,f)),

i.e., such that

∏a,fg(π—Œπ—Žπ—‰(a,f))=e(a,f,Ξ»b.g(f(b))),
∏a,fh(π—Œπ—Žπ—‰(a,f))=e(a,f,Ξ»b.h(f(b))).

Then g and h are equal.

Title 5.3 W-types
\metatable