Erasure of cofixpoints

We describe the state and challenges of translating cofix points and coinductive types to fixpoints.

• The current translation in ECoInductiveToInductive just adds à fun _ => in front of coinductive constructors (fully applied) to thunk them and applies tBox to coinductive scrutinees at cases. tCoFix then translates directly to tFix. This is empirically correct: à cofixpoint can only make recursive calls under a constructor, so evaluation is naturally stuck at the introduced thunk when unfolding the fixpoint. When we force that thunk, we will get a constructor and its corecursive arguments will be stuck again, after reducing the fixpoint in a finite number of steps.

The problem with this translation is that coinductive values in the source language are not necessarily values in the target: a cofixpoint applied to any number of arguments is always a value, but an applied fixpoint might not be. If we use guarded fixpoint evaluation then the only values are partial applications of the fixpoint that don’t include its recursive argument. If we use unguarded fixpoint evaluation then only unapplied fixpoints are values, so it’s impossible to translate cofix to fix in this case. In practice we will reduce the fixpoint’s arguments and unfold it, substituting them in and quickly come to a thunked constructor. We’d like to just have the evaluation of arguments but delay the unfolding part to faithfully emulate cofix with fix

We hence will assume that constructors are eta-expanded and that we use guarded fixpoints and implement a sound translation preserving this. This in turn requires currently that fixpoint applications are eta-expanded. We add the requirement that cofixpoints are also eta-expanded in the source, which means that we store for each cofixpoint its arity / number of arguments before it returns a coinductive value, and every cofix application is full. In that case we can simply thunk cofix applications like we do for constructors:

| mkApps (tCoFix mfix idx) args | = fun _ => mkApps (tFix |mfix| idx) (|args| ++ tBox)

We can set the recursive argument of each fixpoint to the arity of the initial cofixpoint + 1, so the recursive argument is really the tBox marker, to be able to use the fixpoint unfolding evaluation rule. To maintain eta-expanded fixpoints we also need to thunk each corecursive call in mfix which now become recursive calls. Basically this makes every coinductive term start with an explicit lambda, so they are all values. It also freezes the evaluation of the arguments of cofixpoint, which is not what we want.