How to reason about and extract code for inductive types with negative occurrences in Coq?

Question

I'm interested in proving correctness of the interpreter of Appel's compiler (appendix B), and compare it to the machine semantics given by Kennedy on his paper. The interpreter acts as a denotational semantics for the compiler's IR, effectively executing a syntactic object (as a datatype) and returning a computation on the host language. I have a formalization for the machine semantics already (available on GitHub), however, the algorithm is built relying on a type declared (in ML) as:

datatype dvalue = ... | FUNC of dvalue list -> answer | ...

The dvalue type (which is the result type of the interpreter) includes a negative recursive occurrence, which I understand is problematic. So my question is: is there any trick that could be used to formalize the algorithm such that I could still extract executable code from it?

I mean "trick" in the same sense that we can get general recursion by using a coinductive partiality monad, which I was already planning on using anyway since the algorithm does not necessarily terminate. I could, of course, model ML on top of Coq then the algorithm on top of it, but this would be an overkill for reasoning about the algorithm, specially as the extracted code wouldn't really match the original (so I'll leave that as a plan B). Unfortunately, changing this type would deviate too much from the algorithm I'd like to verify and prove correct.

Though I'm asking particularly about Coq (as I've already a bunch of stuff formalized in there...), if this can't be done, could Agda do something like that (perhaps with guarded types)?

Answer 1

Building on Cody's suggestion, the following might work for you. I will consider a simpler type that still captures the essence of the problem.

Define a structure which, given a type answer, produces a type T equivalent to list T -> answer.

Structure Fix (answer : Type) : Type := {
    carrier : Type ;
    f : carrier -> (list carrier -> answer) ;
    g : (list carrier -> answer) -> carrier ;
    fg_id : forall l x, f (g l) x = l x ;
    gf_id : forall y, g (f y) = y
}.

Now, crucially, make sure all the proofs that assume Fix answer do so for an abstract answer, i.e., a parameter can still be instantiated later. Any theorem so proved is consistent because Fix answer is consistent when answer = unit:

Lemma unit_eq : forall x y : unit, x = y.
Proof.
  intros [] []; reflexivity.
Qed.

Definition T : Fix unit.
Proof.
  refine {|
    carrier := unit ;
    f := fun _ _ => tt ;
    g := fun _ => tt
  |}.
  - intros l []; apply unit_eq.
  - apply unit_eq.
Qed.

To put it another way, if you can derive False from S : Fix answer, where answer is a parameter, then you can derive False straight up by instantiating answer := unit and S := T (defined above).

We might worry that in Coq we can prove that S : Fix answer implies answer ≅ unit, which would render the whole thing trivial. But this is not so, because there are semantic models of CIC in which Fix answer is inhabited for non-trivial answer. For example, I would imagine that something like Alex Simpson's Computational adequacy for recursive types in models of intuitionistic set theory would fit the bill.

You will not be able to use anything particular about answer by keeping it general. This should not cause trouble, as it is Appel's intention to keep answer abstract, anyhow.

Answer 2

If I understand you correctly you want to write an interpreter eval: CPS -> dvalue, but the original definition of dvalue was from a non-total programming language, where dvalue occurs in a non-strictl positive position like this, which is not valid in Coq:

data dvalue where
  Int    : int -> dvalue
  String : string -> dvalue
  Not    : (dvalue -> answer) -> dvalue  -- error: dvalue is not strictly positive
  ...

This reminds me of how one can write an interpreter with from an inductively specified language to an denotation specified recursively over its type. But another challenge is that your denotation is untyped. On the other hand the interpreter function should be (easily?) able to generate the type of the value, because every value constructor has a type.

Note that this doesn't mean that the input lanugage (seemingly called CPS) needs to be typed, it can stay untyped, only the dvalues generated by the interpreter should be labelled by the type they belong to.

I suppose the following could work. Define a types of the values:

data ty where
  int  : ty
  str  : ty
  func : ty -> ty
  ans  : ty

define a typed dvalue' recursively over the types

dvalue' : ty -> Type
dvalue' int      = integer
dvalue' str      = string
dvalue' (func s) = dvalue' s -> answer
dvalue' ans      = answer

define untyped dvalue as a typed dvalue' for some type

dvalue : Type
dvalue = Σ (t:ty), dvalue' t

Now eval can be defined as CPS -> dvalue.

The only addition to the untyped eval algorithm is that the types of the produced values need to be labelled by their type. So for example the evaluation of an integer primop, would produce a tuple of the value as specified originally, tagged additionally by an 'int' tag like (int, x+y). The evaluation of an record literal, would produce a tuple of the value as specified originally, tagged additionally by an 'int' tag like (int, x+y).

Now, functions are represented as functions in the denotation, and can be extracted to functions. I hope this helps somehow and I didn't miss any further details.

---

EDIT: The first version of this answer proposed using PHOAS, but that didn't match the question...