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

ho 因此，在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

我们可以得出矛盾。

这些悖论中的一种方法之一就是允许严格的积极递归类型，这就是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，它使用共同的部分类型来实现这一目标。