Quali schemi induttivi possono codificare la seguente definizione AGDA?

Question

Quali schemi di induzione (ad esempio induzione-ricorsione di Dybjer e Setzer, la ricorsione induzione "irlandese" da McBride o induzione induzione da Forsberg e Setzer o forse alcuni più semplici) consentono a uno di codificare la seguente definizione AGDA

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

.

Posso pensare ad alcuni trucchi per riformulare List in questa definizione in modo che la ricorsione di induzione diventa applicabile, ma ci sono schemi che mi permetteranno di dire prima quale sia un elenco e quindi fare riferimento a queste informazioni per dire che il A èIl modo in cui è fatto in AGDA?

Modifica : Come segue dalla risposta di András Kovács, questa definizione particolare può essere riformulata come una famiglia induttiva.Ecco come farlo:

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

Nessun regime che conosco direttamente codifica quel tipo. A volte è chiamato una definizione induttiva "nidificata". La complicazione qui è che Maybe e List sono di tipo costruttori che sono esterni alla firma, e dobbiamo formalizzare la positività severa per gli operatori di tipo esterni in generale, se vogliamo consentire tali definizioni.

In altre parole, la coerenza del A dipende dalla definizione su Maybe e List. Alcuni operatori di tipo esterni non sono positivi, come in:

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

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

.

AGDA Guarda tutte le definizioni esterne e tenta di determinare la varianza dei parametri di tipo. Mentre non conosco un riferimento per una specifica formale diretta di questo, un modo semplice per riformulare definizioni annidate come non annidata è quella di includere gli operatori del tipo esterno in una reciproca firma induttiva. Ad esempio:

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

.

Questo è un normale tipo induttivo reciproco, coperto (dettagli cosmetici Modulo) delle famiglie induttive di Dybjer.