次のAGDA定義をどの誘導方式でエンコードできるか。

Question

どの誘導方式（例えば、DybjerおよびSetzerによる誘導再帰、「アイルランド」誘導 - ForsbergおよびSetzerによる誘導 - 再帰、またはおそらくいくつかのより単純なものである）を許可すると、次のAGDA定義をエンコードすることができます

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

.

誘導再帰が適用可能になるように、この定義のListを再定式化するためにいくつかのトリックを考えることができますが、最初にリストがあることを言うことを可能にするスキームはあります。agdaで終わる方法は？

edit ：AndrásKová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の誘導性家族による覆われた（モジュロ化粧品の詳細）普通の相互誘導型です。