Fixpoints of Indexed Containers

I was going to upload some whiteboard images of the basic constructions for fixpoints of indexed containers, but it won’t let me. I’ll link to them instead.

  • least fixpoint uses W-types for the basic shape, then recursively defined notions of index-matching and input indexing; I didn’t use inductive families because that’s what we’re constructing, right?
  • greatest fixpoint uses M-types for the basic shape, then inductively defined notions of O-indexed and I-indexed places. The index-matching condition is the property that in every O-indexed place, the O you want is the O you’ve got.

Of course, there’s some work to do to show that these things really are what I say they are, but I think they look about right.

By the by, we really need to figure out some notational issues or we’re heading for a mess…

5 Responses to “Fixpoints of Indexed Containers”

  1. Conor Says:

    Dr Hancock happened to be passing, whereupon he reminded me that large eliminations are locally considered to be cheating. He further reminded me that someone had written a lump of Epigram which did it without large eliminations. I shall fix this presently.

  2. Conor Says:

    OK folks, how about this?

  3. Conor Says:

    And, moreover, I’ve done the fixpoint construction in Epigram (with ext as an axiom). I’ve written both directions of the iso, but not the proof that it is an iso. The code is here.

  4. Hank Says:

    I looked at the Petersson-Synek paper “A set constructor for inductive sets in Martin-Löf’s type theory” (from 1989 which you can find on Kent’s page). I notice that in section 4 of that paper, it is mentioned that Dan actually proved that their `tree-set’ principle can be reduced to W-types. The reference given is to a Chalmers technical report that does not seem to be online.

    “Deriving rules for inductive sets in Martin-Löf’s type theory” also from 1989.

    The approach (only sketched) is to pick out “good” trees in a W-type. Unfortunately it isn’t possible to tell how this predicate is defined. Conceivably though he used the method given above (but to me it seems more likely he used a `large elimination’).

    In any case, the next time someone is in Chalmers, could they please ask for a copy of this report? Or if they bump into Dan somewhere?

  5. Conor Says:

    Curious. I’ve just updated the pdf of the fixpoint stuff with something of the story which I hacked. Don’t know if it makes sense.

Leave a Reply

You must be logged in to post a comment.