The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Thorsten,

Now that you explain it that way, I feel like it should have been obvious… :)

Thanks for the example!

-Eddy

On Jul 14, 2015, at 7:35 AM, Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

Hi Eddy,

By induction-induction we mean the mutual inductive definition of a type A and a type B depending on A where constructors may appear in the types of later constructors. The canonical example is

data Con  : Set

data Ty   : Con → Set

data Con where

  •       : Con  

  _,C_    : (Γ : Con) → Ty Γ → Con

data Ty where

  U       : ∀{Γ} → Ty Γ

  Π       : ∀{Γ}(A : Ty Γ)(B : Ty (Γ ,C A)) → Ty Γ

More generally, I should say induction-induction is the mutual definition of any number of datatypes which may depend on each other. 

I should add that while the syntax of inductive-inductive types in Agda is quite general it does not (yet) allow the occurrence of constructors in any order (but constructors for the same type have to be defined together).

I conjecture that the proof-thoretic strength of strictly positive inductive-inductive definition is the same as for ordinary strictly positive inductive definitions.

Thorsten

From: Eddy Westbrook <westbrook AT kestrel.edu>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Tuesday, 14 July 2015 15:27
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Faking induction-induction in Coq?

All,

I thought that induction-recursion greatly increases the proof-theoretic strength of a system, because it allows building an inductive encoding of the types of the system in the system itself, which in turn allows one to build a model of the system (without I-R). This makes it seem to me like this is not a trivial extension...

Is this not the case here? Maybe I do not understand the difference between induction-recursion and what you are calling induction-induction?

-Eddy

On Jul 14, 2015, at 6:01 AM, Fredrik Nordvall Forsberg <fredrik.nordvall-forsberg AT strath.ac.uk> wrote:

Hi Bas,

On 13/07/15 19:49, Bas Spitters wrote:

So why are they not included in Coq?

Are you really claiming that there is a detailed semantics for
CIC+IndInd and that all the meta-theory has been done?
I agree, it should work. However, I haven't seen the details yet.

The classical set-theoretic semantics of MLTT + inductive-inductive
definitions should extend to an impredicative Prop very
straightforwardly. However, you are right that there are no proofs of
e.g. normalization for this theory (or for induction-recursion, for that
matter). I would expect this to work with no problems.

Best regards,
Fredrik

On Mon, Jul 13, 2015 at 7:59 PM, Thorsten Altenkirch
<Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

Hi Jason,

afaik there is no easy way to do this. I discussed this recently with
Frederik Forsberg, whose PhD thesis is a good source of information about
induction-induction. See section 5.3.

You can approximate inductive-inductive definition using a similar technique
as for induction-recursion but you don’t get the right eliminator. E.g. If
you define a family A : Set, B : A -> Set you expect that the elimination
operators have the form

elim-A : (X : Set)(Y : X -> Set) -> … -> A -> X
elim-B : (X : Set)(Y : X -> Set) -> … -> (a : A) -> B a -> Y (elim-A X Y …
a)

the problem here is the dependency of the 2nd operator on the first.

However, unlike the problem with univalence and extensionality this one is
relatively easy to fix as Agda shows. Inductive-inductive definitions have a
straightforward operational semantics and also it is no problem to derive
eliminators and recursors for them. So why are they not included in Coq?

Thorsten

From: Jason Gross <jasongross9 AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Sunday, 12 July 2015 04:58
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Faking induction-induction in Coq?

Hi,
Is there a (known) way to fake induction-induction in Coq?

Abhishek mentioned
http://www.cs.ru.nl/~venanzio/publications/induction_recursion.ps last year
as a way of faking induction-recursion in Coq.  I'm curious, in particular,
about how to define well-typed syntax for dependent type theory in Coq, and,
more specifically, one that supports a quotation function, which sends any
syntactic term to a syntactic representation of that syntax, i.e., sends
(app 'S' '0'), the syntax representing the numeral 1, to (app (app 'app'
"S") "0").

Thanks,
Jason

-- 
Fredrik Nordvall Forsberg,
Department of Computer and Information Sciences,
University of Strathclyde.
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.

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.