AGDAの「厳密に肯定的」

Question

Haskellで書いたプログラムに基づいて、いくつかの表示セマンティクスをAGDAにエンコードしようとしています。

data Value = FunVal (Value -> Value)
           | PriVal Int
           | ConVal Id [Value]
           | Error  String

AGDAでは、直接的な翻訳は次のとおりです。

data Value : Set where
    FunVal : (Value -> Value) -> Value
    PriVal : ℕ -> Value
    ConVal : String -> List Value -> Value
    Error  : String -> Value

しかし、Funvalに関連するエラーが発生します。

値は、値の定義においてコンストラクターFunvalのタイプで矢の左に発生するため、厳密に肯定的ではありません。

これは何を意味するのでしょうか？これをAGDAでエンコードできますか？私はそれについて間違った方法で進んでいますか？

ありがとう。

Answer 1

ホア このため、AGDAでは機能しません。

apply : Value -> Value -> Value
apply (FunVal f) x = f x
apply _ x = Error "Applying non-function"

w : Value
w = FunVal (\x -> apply x x)

さて、評価することに注意してください apply w w あなたにあげる apply w w 再び。用語 apply w w AGDAのノーノーである通常のフォームはありません。このアイデアとタイプを使用してください。

data P : Set where
    MkP : (P -> Set) -> P

矛盾を導き出すことができます。

これらのパラドックスから抜け出す方法の1つは、厳密に肯定的な再帰タイプを可能にすることだけです。これがAGDAとCOQが選択するものです。つまり、宣言した場合：

data X : Set where
    MkX : F X -> X

それか F 厳密にポジティブな施設である必要があります。 X 矢印の左側には発生しない可能性があります。したがって、これらのタイプは厳密に肯定的です X:

X * X
Nat -> X
X * (Nat -> X)

しかし、これらは次のとおりです。

X -> Bool
(X -> Nat) -> Nat  -- this one is "positive", but not strictly
(X * Nat) -> X

要するに、AGDAのデータ型を表すことはできません。 de bruijnエンコードを使用して作業できる用語タイプを取得できますが、通常、評価関数には、AGDAがすべての機能を必要とするため、評価するための最大数のステップ数（一般的に「燃料」と呼ばれる）が必要です。合計する。 これが例です @gallaisのために、これを達成するために共誘導性の偏見型を使用しています。