The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

The solutions pointed out by others are great. There is another one that that I wrote about on my blog a little while ago where you approximate Mu using fixpoints.

http://gmalecha.github.io/reflections/2016/01/14/approximating-inductive-types/

The basic idea is to index Mu by a natural number that unfolds F some number of times, i.e.

Variable F : Type -> Type.

Fixpoint Mu (n : nat) :=

  match n with

  | 0 => Empty_set

  | S n => F (Mu n)

  end.

The blog post shows some examples for writing eliminators and such for types like this.

On Wed, Mar 30, 2016 at 7:46 AM, Igor Zhirkov <igorjirkov AT gmail.com> wrote:

Hello, 

I wonder whether it is possible to define the Mu  combinator in Coq in a general way. 

In Haskell it can be defined like that: 

>>>

newtype Fix f = Fx (f (Fix f ) )

<<<

Or like that (using records syntax):

>>>

newtype Mu f = In {out :: f (Mu f)}

<<<

When translated directly into Coq it fails with "Non strictly positive occurrence of Mu":

>>>

Inductive Mu f := MIn {MOut: f ( Mu f) }.   

<<<

Maybe I need to throw in some axioms to work around the termination issues?

It seems, however, that for an arbitrary recursive type one can always write a definition that corresponds to the Mu application to the corresponding functor:

>>>

Inductive exprf a :=

| add : a -> a -> exprf a

| lit: nat -> exprf a.

Inductive expr := In { Out: exprf expr }.

<<<

While doing a little research I have only stepped on the work of Arthur Chargueraud  (A Practical Fixed Point Combinator for Type Theory), but it does not seem to me that it is relevant.

What I am trying to achieve is the separation of the recursion schema and the computable part (algebra) for catamorphisms and anamorphisms.

BR

Igor

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/