10
$\begingroup$

W-types are said to be "a well-founded inductive type" that is parameterized over arities and constructors, similar to a "tree of possible constructions". On nlab, it is said that a lot of inductive types can be encoded with W-type.

However, from that description I still don't understand what's well-foundedness in terms of the syntax of inductive types. I can see that Agda's non-mutual inductive families are "well-founded" because it's a rooted tree, but what about inductive-recursive and inductive-inductive types? I think these are known to be not equivalent to non-mutual inductive families and they have a more complex model. I think someone told me that strictly positive inductive families are well-founded, but what exactly makes a(n inductive) type well-founded?

Can we encode all well-founded inductive types with the W-type?

$\endgroup$
3
  • 1
    $\begingroup$ Are you asking about the mathematical meaning of "well-founded", or why inductive types from proof assistants should be thought of consisting of well-founded trees? Note that "well-founded inductive type" is a pleonasm: "well-founded" and "inductive" are more or less two facets of the same thing. $\endgroup$ Mar 2, 2022 at 12:25
  • $\begingroup$ @AndrejBauer Probably the meaning of well-foundedness in terms of type theory. For example, I am having trouble visualizing I-R elimination as a rooted tree (I am ok with simpler inductive types) $\endgroup$
    – ice1000
    Mar 2, 2022 at 15:16
  • 1
    $\begingroup$ The inductive part of induction-recursion defines trees similar to other inductive definitions. The specification of the shape is just more flexible. The contents of an inductive constructor is a telescope, so later fields can be drawn from families depending on earlier ones. This can't happen for recursive fields in ordinary inductive types, though, because no families depend (non-trivially) on the type being defined yet. Induction-induction and induction-recursion give two ways of making this happen. $\endgroup$
    – Dan Doel
    Mar 2, 2022 at 17:21

1 Answer 1

13
$\begingroup$

"Well-founded" and "inductive" mean roughly the same thing. I think the reason different terminology tends to get used for W-types is that their definition looks similar to notation for ordinals (imagining that the branching of the trees is like a limit of the children). They're distinct from the other inductive types given in Martin-löf type theory in that they are potentially infinitely wide. But they're still supposed to be (intuitively) finitely deep, which is what the "inductive" and "well-founded" refer to

Whether or not you can encode various other sorts of inductively specified types as W-types is a complicated question.

  1. It's pretty easy to show that you can encode plain inductive types using W-types if you have various sorts of extensionality. The typical schemas for what constitutes an 'inductive definition' are like finite polynomials, while W-types are trees built from any (infinite) polynomial definable in type theory. The main discrepancy is how the 'products' act. The finite products in inductive schemas have a canonical form, while the functions used in W-types do not, and the most obvious way to fix that is with function extensionality.

  2. However, you can also get by without extensionality. You only need some eta rules. The idea is to use W-types to build the right sort of trees, then define the subtype of 'canonical' trees by (W-type) induction. It happens that the recursion rule for this subtype has the judgmental behavior matching the schema for inductive definitions.

  3. You can also encode indexed W-types using normal W-types and the identity type using a similar strategy. You use W-types to build a larger type of trees on the 'total spaces' involved, and then define a subtype of well-indexed trees by induction. This file shows how to do it.

  4. You can (I believe) encode indexed inductive types/families using indexed W-types, including the encoded version of those, using a strategy similar to the Why Not W? paper. My Agda file above shows how to do this for a fairly simple indexed type that was mentioned in another question here.

  5. You can encode mutual inductive and inductive-inductive types with indexed inductive types. For mutual inductive types, you just add a finite index type to turn N definitions into a single N-indexed definition. For induction-induction, you follow a similar strategy as for building indexed W-types: define mutual inductive types that contain too many values, then define the subtypes with proper indexing afterward.

  6. You cannot encode all inductive-recursive definitions as (indexed) inductive definitions. I-R definitions were invented as a schema that would let you write down the definition of universes as a special case. However, the additional power comes from simultaneously being able to define a recursive type family. If instead you just simultaneously define a recursive function into an existing type, I believe they are encodable using a strategy like above. This might mean that if you have enough universes, you can use them with inductive definitions to encode everything you could write by just having a theory that admits inductive-recursive definitions (but with no pre-specified universes). I'm unsure about this, though.

  7. Having a universe that classifies inductive-recursive definitions is even stronger, and isn't itself an instance of induction-recursion. It's actually inconsistent to be able to do induction on such a universe (while the I-R definable universes in 6 can have an associated induction principle).

  8. Quotient/higher inductive types can't be encoded as any of the previous sorts of definition in general. Quotients where you can compute a canonical representative for each equivalence class can be defined, but not all quotients are like that.

I don't think strict positivity has anything to do with being inductive/well-founded (negativity does, though; see the comments). It's necessary to guarantee that 'all' inductive definitions are meaningful in various sorts of models. For instance, you can't have a classical set theoretic model of an inductive type $T \cong 2^{2^T}$ (which is positive, but not strictly positive), because $2$ classifies the propositions, and you can't have a type equivalent to its double power type. Constructively you might be able to admit some such types, and for instance, $λ \_ → 0$ and $λ\_ → 1$ give you a starting point for building up your finitely-deep values. However, these sorts of non-strictly positive types can conflict with other features than just classical mathematics, so you need to be very careful.

Various bits of the above are subject to caveats about the details of what counts as an "inductive definition." There's literature out there rigorously defining various schemata for what constitutes an (indexed) inductive(-recursive/inductive) definition (etc.). Agda (for instance) is not super rigorous, and runs a checker that lets you conveniently do things that could probably be encoded in those more rigorous schemata in a more inconvenient way. Or perhaps you couldn't, but it's still fine; or isn't.

$\endgroup$
4
  • 1
    $\begingroup$ I wouldn’t say (strict) positivity has nothing to do with being well-founded: from what I understand, positivity exactly characterizes well-founded inductive types, and strict positivity is a convenient restriction of this. As far as I know, the encodings into W types you mention work only for (strictly) positive definitions. $\endgroup$ Mar 2, 2022 at 9:27
  • 1
    $\begingroup$ Also, there is a line of work on using equality to encode indexed inductive types by (amongst others) McBride (see his PhD thesis for instance, where the reference to Henry Ford’s "You can have any color you like, as long as it’s black." often used when talking about this technique goes back to, afaik). $\endgroup$ Mar 2, 2022 at 9:36
  • 1
    $\begingroup$ Yeah, (not necessarily strict) positivity is connected to well-foundedness in most theories because negativity would allow you to define non-well-founded things by (essentially) diagonalization. I think a theory where everything was linear wouldn't be affected (same way it avoids Russel's paradox). But I don't even know what such a setting would really be like. I can correct my answer to hopefully make that more clear. $\endgroup$
    – Dan Doel
    Mar 2, 2022 at 16:40
  • $\begingroup$ Hmm, given your familiarity with "conflicting features", might you be able to answer this question? $\endgroup$
    – user21820
    Nov 29, 2022 at 7:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.