Welche induktiven Schemata können die folgende Agda-Definition kodieren?

Question

Welche Induktionsschemata (z.B.Induktionsrekursion von Dybjer und Setzer, „irische“ Induktionsrekursion von McBride oder Induktionsinduktion von Forsberg und Setzer oder vielleicht einige einfachere) ermöglichen es einem, die folgende Agda-Definition zu kodieren

  data A : Set where
    a : Maybe (List A) → A

Mir fallen einige Tricks zur Umformulierung ein List in dieser Definition, damit die Induktionsrekursion anwendbar wird, aber gibt es Schemata, die es mir ermöglichen würden, zuerst zu sagen, was eine Liste ist, und mich dann auf diese Informationen zu beziehen, um zu sagen, was? A Ist das in Agda so?

Bearbeiten:Wie aus der Antwort von András Kovács hervorgeht, dies besondere Die Definition kann als induktive Familie umformuliert werden.So geht's:

data Three : Set where one two three : Three

data AG : Three → Set where
  a'       : AG three → AG one
  nil'     : AG two
  cons'    : AG one → AG two → AG two
  nothing' : AG three
  just'    : AG two → AG three

A = AG one
ListA = AG two
MaybeListA = AG three

a : MaybeListA → A
a = a'

nil : ListA
nil = nil'

cons : A → ListA → ListA
cons = cons'

nothing : MaybeListA
nothing = nothing'

just : ListA → MaybeListA
just = just'

Answer 1

Kein mir bekanntes Schema kodiert diesen Typ direkt.Manchmal wird es eine „verschachtelte“ induktive Definition genannt.Die Komplikation hier ist, dass Maybe Und List sind Typkonstruktoren, die außerhalb der Signatur liegen, und wir müssen für externe Typoperatoren im Allgemeinen eine strikte Positivität formalisieren, wenn wir solche Definitionen zulassen wollen.

Mit anderen Worten, die Konsistenz von A hängt von der Definition ab Maybe Und List.Einige externe Typoperatoren sind nicht positiv, wie zum Beispiel:

data Neg (A : Set) : Set where
  neg : (A -> Bool) -> Neg A

data B : Set where
  b : Neg B -> B

Agda untersucht alle externen Definitionen und versucht, die Varianz der Typparameter zu bestimmen.Obwohl mir keine Referenz für eine direkte formale Spezifikation hierfür bekannt ist, besteht eine einfache Möglichkeit, verschachtelte Definitionen als nicht verschachtelt umzuformulieren, darin, die externen Typoperatoren in eine gegenseitige induktive Signatur einzubeziehen.Zum Beispiel:

data A : Set 
data ListA : Set
data MaybeListA : Set

data A where
  a : MaybeListA -> A

data ListA where
  nil : ListA
  cons : A -> ListA -> ListA

data MaybeListA where
  nothing : MaybeListA
  just : ListA -> MaybeListA

Dies ist ein gewöhnlicher gegenseitiger Induktionstyp, der (modulo kosmetische Details) von Dybjers Induktionsfamilien abgedeckt wird.