다음 Agda 정의를 인코딩할 수 있는 귀납적 체계는 무엇입니까?

Question

어떤 유도 방식(예:Dybjer 및 Setzer의 유도-재귀, McBride의 "Irish" 유도-재귀 또는 Forsberg 및 Setzer의 유도-귀납 또는 아마도 더 간단한 것)을 사용하면 다음 Agda 정의를 인코딩할 수 있습니다.

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

재구성할 수 있는 몇 가지 트릭을 생각해 볼 수 있습니다. List 귀납-재귀가 적용 가능하도록 이 정의에서 먼저 목록이 무엇인지 말한 다음 이 정보를 참조하여 무엇인지 말할 수 있는 체계가 있습니까? A Agda에서는 그런 식으로 진행되나요?

편집하다:András Kovács의 답변에서 다음과 같이 특정한 정의는 귀납적 가족으로 재구성될 수 있다.수행 방법은 다음과 같습니다.

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

내가 아는 어떤 체계도 해당 유형을 직접 인코딩하지 않습니다.때때로 그것은 "중첩된" 귀납적 정의라고 불립니다.여기서 복잡한 점은 Maybe 그리고 List 시그니처 외부에 있는 유형 생성자이며, 그러한 정의를 허용하려면 일반적으로 외부 유형 연산자에 대해 엄격한 긍정성을 공식화해야 합니다.

즉, 일관성은 A 정의에 따라 달라집니다. Maybe 그리고 List.다음과 같이 일부 외부 유형 연산자는 양수가 아닙니다.

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

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

Agda는 모든 외부 정의를 조사하고 유형 매개변수의 변화를 확인하려고 시도합니다.이에 대한 직접적인 공식 사양에 대한 참조는 모르지만 중첩된 정의를 중첩되지 않은 것으로 다시 공식화하는 쉬운 방법은 외부 유형 연산자를 상호 귀납적 서명에 포함시키는 것입니다.예를 들어:

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

이것은 Dybjer의 유도 제품군에 의해 다루어지는(모듈로 외관 세부 사항) 일반적인 상호 유도 유형입니다.