28

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 に関連するエラーが発生します。

Value は、Value の定義のコンストラクター FunVal の型の矢印の左側にあるため、厳密には正ではありません。

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

ありがとう。

4

1 に答える 1

34

次の理由により、 HOASは 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 による例です。

于 2010-04-06T09:04:40.577 に答える