The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

You need a stronger assumption on f to ensure termination because otherwise you could have

f x = x -> x

and this would give you untyped lambda calculus and hence non-termination. First of all you want to eliminate the possibility of negative occurences, I.e. you need to require that f is a functor (you need this anyway even in Haskell if you want to define the fold for the datatype). However, even this requirement leaves you with some stratnge types which are not definable in Coq, such as

f x = (x -> bool) -> bool

While accepting these sort of types doesn’t directly lead to non-termination they is no goo justification in my view why they should exist. Instead of positivity (withnessed by f being a functor) you want strict positivity which can be witnessed by f being a container, that is there is

S : Set

P : S -> Set

such that

f x = Sigma s:S. P s -> x

then Mu f exist and it is called a W-type. For more details on containers see for example

http://www.cs.nott.ac.uk/~psztxa/publ/cont-tcs.pdf

or for a more paedagogical introduction, see section 5 of

http://www.cs.nott.ac.uk/~psztxa/publ/ssgp06.pdf

Thorsten

From: Igor Zhirkov <igorjirkov AT gmail.com>
Reply-To: <coq-club AT inria.fr>
Date: Wed, 30 Mar 2016 16:46:57 +0200
To: <coq-club AT inria.fr>
Subject: [Coq-Club] Mu combinator

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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.