coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mu combinator

From: "John Wiegley" <johnw AT newartisans.com>
To: "Igor Zhirkov" <igorjirkov AT gmail.com>
Cc: "" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Mu combinator
Date: Wed, 30 Mar 2016 08:44:21 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f179.google.com
Ironport-phdr: 9a23:DoTk7RIB6YBcwPdw1tmcpTZWNBhigK39O0sv0rFitYgUL/XxwZ3uMQTl6Ol3ixeRBMOAu6IC0bqd4/GocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC34Lth6viqtX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVG4T1eL5wf7xZFjchLSp9sMzksgPBTBGM4WU0XWAfkx4OCA/AukLURJD052HYsep7kBabMMLyQKF+EWCg6KdtVzfuhTgOLSI462jRkYp7i6cN80HpnAB234OBONLdD/F5ZK6IJd4=
Organization: New Artisans LLC

>>>>> Igor Zhirkov
>>>>> <igorjirkov AT gmail.com>
>>>>> writes:

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

Hi Igor,

In many cases you can use a "Mendler-style Church encoding" of Mu:

Definition Mu (f : Type -> Type) :=
forall r, (forall x, (x -> r) -> f x -> r) -> r.

Note that you only need to know f is a Functor at reduction time.

However: this "Mu" may be "larger" in CiC than f (Mu f), which could have
implications for what you're doing.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Mu combinator, Igor Zhirkov, 03/30/2016
- Re: [Coq-Club] Mu combinator, Thorsten Altenkirch, 03/30/2016
- Re: [Coq-Club] Mu combinator, John Wiegley, 03/30/2016
  - Re: [Coq-Club] Mu combinator, Thorsten Altenkirch, 03/30/2016
    - Re: [Coq-Club] Mu combinator, John Wiegley, 03/30/2016
- Re: [Coq-Club] Mu combinator, Gregory Malecha, 03/31/2016