归约关系的孔内可能以多种不同方式匹配孔

Question

我有一种使用 PLT-Redex 定义的语言，它具有（动态）混合类型。表达式如下所示：

; terms / expressions
(e ::= x
     (lkp e f)
     (call e m e ...)
     (new C e ... ⊕ (e R e ...) ...)
     (bind x ... with (e R e ...) ... from y ... e))

; values
(v ::= (new C v ... ⊕ (v R v ...) ...))

语言的评估是通过 w.r.t. 完成的。评估上下文和归约关系。

; evaluation contexts
(E ::= hole
   (lkp E f) ; CR-FIELD
   (call E m e ...) ; CR-INVK
   (call v m v ... E e ...) ; CR-INVK-ARG
   ;(new C v ... E e ... ⊕ (e R e ...) ...)
   ;(new C v ... ⊕ (E R e ...) ...)
   ;(new C v ... ⊕ (v R v ... E e ...) ...)
   (bind x ... with (E R e ...) ... from y ... e)
   (bind x ... with (v R v ... E e ...) ... from y ... e))

我的归约关系目前仅针对字段访问 (lkp) 定义，它将对 mixin 的查找归约到其值。

(define red
  (reduction-relation
   fej
   #:domain (e CT)
   ;R-FIELD
   (--> ((in-hole E (lkp (new C v_0 ... ⊕ (v_1 R v_2 ...) ...) f_i)) CT)
        ((in-hole E v_i) CT)
        "(R-FIELD)"
        (where v_i (fvalue CT f_i (new C v_0 ... ⊕ (v_1 R v_2 ...) ...))))
   ))

我对我的元函数 (fvalue) 进行了测试，以验证它们是否有效。然而，redex 告诉我，我的归约关系以许多不同的方式映射到一个洞。我是否为new C ... 评论不同版本的评估上下文并不重要。错误来自this place。

reduction-relation: in-hole's first argument is expected to match exactly one hole, but it may match a hole many different way

如何调试（或修复）问题？通常，我使用 Emacs 和 Racket 模式进行开发，或者使用 DrRacket。问题是当使用宏步进器时，错误会从一个步骤抛出到另一个步骤。如果我能看到它捕获的孔甚至了解它失败的地方，那就太好了。所以我也许明白为什么它完全失败了。

Answer 1

如果我使用以下上下文定义定义语言（为简单起见，我将使用类似λ 的语言），我会得到同样的错误：

(E hole
   (E e ...)
   (v E ...))  ;; <-- problem

这意味着，例如，以下是E 上下文：

((lambda (x y) x) hole hole)

但是 (IIUC) Redex（或至少 reduction-relation）不允许具有多个孔的上下文，因此它会抱怨。

您的代码中的问题似乎出在E 的最后两个产生式中，其中E 出现在后面跟着省略号的模式内。 （其中一个被注释掉的E 作品也有同样的问题。）