Racket、PLT Redex、测试-->E 不存在

Question

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

Answer 1

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

#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.