“严格肯定”在Agda [英] "Strictly positive" in Agda

问题描述

  data数值= FunVal（价值 - >价值）
 | PriVal Int 
 | ConVal Id [Value] 
 |错误字符串
  

在Agda中，直接翻译将是;

  data数值：设置其中
 FunVal：（值 - >值） - >价值
 PriVal：ℕ - >价值
 ConVal：字符串 - >列表值 - >价值
错误：字符串 - >价值
  

但我得到一个与FunVal有关的错误，因为;

值不是严格正数，因为它出现在
Value定义中的构造函数FunVal类型中的
箭头的左侧。 / p>

这是什么意思？我可以在Agda中编码吗？

谢谢。

解决方案

HOAS 在Agda中不起作用，因为这个原因：

  apply：Value  - >价值 - >价值
 apply（FunVal f）x = fx 
 apply _ x =错误Applying non-function
 
w：Value 
w = FunVal（\ x  - > ; apply xx）
  

现在请注意，评估应用ww 给你再次应用ww 。术语申请w w 没有任何正常形式，这在agda中是不可以的。使用这个想法和类型：

  data P：Set where 
 MkP：（P  - > Set） - > P 
  

我们可以推导出一个矛盾。

这些悖论之一的出路在于只允许严格的递归类型，这是Agda和Coq选择的类型。这意味着，如果您声明：

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

F 必须严格为正值functor，这意味着 X 可能永远不会出现在任何箭头的左侧。因此，这些类型在 X 中严格为正：

  X * X 
 Nat  - > X 
 X *（Nat  - > X）
  

但这些不是： p>

  X  - > Bool 
（X  - > Nat） - >纳特 - 这一个是积极的，但不是严格的
（X * Nat） - > X 
  

因此，简而言之，您不能在Agda中表示您的数据类型。如果您打算评估条款，de Bruijn编码也不起作用。您无法将无类型的lambda微积分嵌入到Agda中，因为它具有没有正常形式的条款，并且Agda要求所有程序正常化。

I'm trying to encode some denotational semantics into Agda based on a program I wrote in Haskell.

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

In Agda, the direct translation would be;

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

but I get an error relating to the FunVal because;

Value is not strictly positive, because it occurs to the left of an arrow in the type of the constructor FunVal in the definition of Value.

What does this mean? Can I encode this in Agda? Am I going about it the wrong way?

Thanks.

解决方案

HOAS doesn't work in Agda, because of this:

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

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

Now, notice that evaluating apply w w gives you apply w w back again. The term apply w w has no normal form, which is a no-no in agda. Using this idea and the type:

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

We can derive a contradiction.

One of the ways out of these paradoxes is only to allow strictly positive recursive types, which is what Agda and Coq choose. That means that if you declare:

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

That F must be a strictly positive functor, which means that X may never occur to the left of any arrow. So these types are strictly positive in X:

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

But these are not:

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

So in short, no you can't represent your data type in Agda. And de Bruijn encoding won't work either if you are going to evaluate terms. You can't embed the untyped lambda calculus into Agda because it has terms without normal forms, and Agda requires all programs to be normalizing.

这篇关于“严格肯定”在Agda的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！