I gave a brief talk today on the quotation work I'd been doing in MetaCoq, here is the slide deck for anyone interested.

was there an obvious reason for the "else" on slide 3 in Agda? (Interested in if this was due to Agda features or someone had done previous work)

@Karl Palmskog What do you mean "the 'else' on slide 3"? (I don't quite understand the question.)

What I have in Agda (from another project I was working on) is a formalization of Löb's Theorem from an abstract category of syntax based on a generalization of Lawvere's fixpoint theorem. This is sort-of the complement of the work in MetaCoq: a proof of Löb's Theorem that does not commit to a particular AST but tries to be more-or-less compatible with any tree you might pick. There's a rough sketch of the (non-reduction) building blocks / assumptions on slides 9--12, though the Agda source is a more complete (if a bit less readable) list.

The assumptions fall into one of four categories:

- adding a layer of quotation (what I worked on in MetaCoq)
- decidable equality of syntax trees (also done in MetaCoq)
- assumptions that are (I claim) obviously straightforward (things like
`(□ A × □ B) → □(A × B)`

) - assumptions that are about reduction behavior (which I've not thought much about the difficulty of; but these are only needed for establishing that Löb's Theorem produces a fix point (unfortunately this is needed even in the computational part when using the diagonal lemma to discharge some assumptions of Löb's Theorem though))

Does this answer your question?

I was referring to the "Everything else is comparatively straightforward; details (and Agda formalization) available", yes. So you answered my question with the Agda link, thanks.

Last updated: Jul 23 2024 at 21:01 UTC