Racket, PLT Redex, test-->E non existence

Question

I'm trying to prepare semantics for a language. Some derivation may lead to a 'stuck' state. I want to have a test, what certain term can't be reduced to the 'stuck' state. Is it somehow possible to represent it using something like test-->E?

Answer 1

Here is an example adapted from the λv example on the Redex page but with a stuck state added. Is this helpful to you?

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