Racket, PLT Redex, test-->E 不存在答案

【问题标题】：Racket, PLT Redex, test-->E non existenceRacket, PLT Redex, test-->E 不存在
【发布时间】：2015-10-25 14:18:03
【问题描述】：

我正在尝试为一种语言准备语义。一些推导可能会导致“卡住”状态。我想做一个测试，某个术语不能被简化为“卡住”状态。是否有可能使用test-->E 之类的东西来表示它？

【问题讨论】：

是的，如果您的语法中有明确的卡住术语，您可以使用test-->E。 test-->E 是否有一些你无法工作的具体问题？显然，如果您给test-->E 一个非终止程序，您的测试将不会完成，除非您将测试限制在有限的步骤中。
实际上我正在尝试进行测试，以证明stuck 状态没有派生。是的，我有明确的术语。没关系，如果解决方案仅适用于终止程序。但我认为它也应该适用于 Redex 可以找到固定点的程序。说到test-->E，我想要test-->notE之类的东西。
另外我应该补充一点，我的语义是非确定性的，所以在这种情况下使用test-->> 并列出所有非卡住状态是很痛苦的。
我也有点错误：在上述所有情况下，您都应该将--> 读作-->>。
如果假设终止没问题，那么为了测试减少没有卡住，你可以检查它是否减少到一个值？

标签： racket plt-redex

【解决方案1】：

这是一个改编自 λv example on the Redex page 的示例，但添加了 stuck 状态。这对您有帮助吗？

#lang racket
(require redex)

(define-language λv
  (e (e e ...) (if0 e e e) x v stuck)
  (v (λ (x ...) e) n +)
  (n natural)
  (E (v ... E e ...) (if0 E e e) hole)
  (x (variable-except λ + if0)))

(define red
  (reduction-relation
   λv
   (--> (in-hole E (+ n_1 n_2))
        (in-hole E ,(+ (term n_1) 
                       (term n_2)))
        "+")
   (--> (in-hole E (if0 0 e_1 e_2))
        (in-hole E e_1)
        "if0t")
   (--> (in-hole E (if0 number_1 e_1 e_2))
        (in-hole E e_2)
        "if0f"
        (side-condition 
          (not (= 0 (term number_1)))))
   (--> (in-hole E ((λ (x ..._1) e) v ..._1))
        (in-hole E (subst-n (x v) ... e))
        "βv")
   (--> (in-hole E (n v ..._1))
        stuck
        "βv-err")))

(define-metafunction λv
  subst-n : (x any) ... any -> any
  [(subst-n (x_1 any_1) (x_2 any_2) ... any_3)
   (subst x_1 any_1 (subst-n (x_2 any_2) ... 
                             any_3))]
  [(subst-n any_3) any_3])

(define-metafunction λv
  subst : x any any -> any
  ;; 1. x_1 bound, so don't continue in λ body
  [(subst x_1 any_1 (λ (x_2 ... x_1 x_3 ...) any_2))
   (λ (x_2 ... x_1 x_3 ...) any_2)
   (side-condition (not (member (term x_1)
                                (term (x_2 ...)))))]
  ;; 2. general purpose capture avoiding case
  [(subst x_1 any_1 (λ (x_2 ...) any_2))
   (λ (x_new ...) 
     (subst x_1 any_1
            (subst-vars (x_2 x_new) ... 
                        any_2)))
   (where (x_new ...)
          ,(variables-not-in
            (term (x_1 any_1 any_2)) 
            (term (x_2 ...))))]
  ;; 3. replace x_1 with e_1
  [(subst x_1 any_1 x_1) any_1]
  ;; 4. x_1 and x_2 are different, so don't replace
  [(subst x_1 any_1 x_2) x_2]
  ;; the last cases cover all other expressions
  [(subst x_1 any_1 (any_2 ...))
   ((subst x_1 any_1 any_2) ...)]
  [(subst x_1 any_1 any_2) any_2])

(define-metafunction λv
  subst-vars : (x any) ... any -> any
  [(subst-vars (x_1 any_1) x_1) any_1]
  [(subst-vars (x_1 any_1) (any_2 ...)) 
   ((subst-vars (x_1 any_1) any_2) ...)]
  [(subst-vars (x_1 any_1) any_2) any_2]
  [(subst-vars (x_1 any_1) (x_2 any_2) ... any_3) 
   (subst-vars (x_1 any_1) 
               (subst-vars (x_2 any_2) ... any_3))]
  [(subst-vars any) any])


(define not-stuck? (redex-match λv v))
(define stuck? (redex-match λv stuck))
(test-->>E red (term (+ 1 2)) not-stuck?)
(test-->>E red (term (1 2)) stuck?)
(test-results) ; => Both tests passed.

【讨论】：