试图用redex定义一种小语言

Question

我正在关注Redex的amb tutorial，并且同时为皮尔斯类型和编程语言中的类型化算术表达式构建了一个模型。

我已经定义了这种小语言的语法和类型系统，但我很难定义它的小步语义。在我解决问题之前，让我介绍一下迄今为止的定义。

首先，我定义了语言的语法。

(define-language ty-exp 
    [E (ttrue) 
     (ffalse) 
     (zero) 
     (suc E) 
     (ppred E) 
     (iszero E) 
     (iff E E E)] 
    [T (nat) 
    (bool)]) 

接下来，我定义了没有问题的类型系统。

(define-judgment-form ty-exp 
    #:mode (types I O) 
    #:contract (types E T) 

    [ 
    ----------------------"T-zero" 
    (types (zero) (nat)) 
    ] 

    [ 
    -------------------------- "T-false" 
    (types (ffalse) (bool)) 
    ] 

    [ 
    -------------------------- "T-true" 
    (types (ttrue) (bool)) 
    ] 

    [ 
    (types E (nat)) 
    -------------------------- "T-suc" 
    (types (suc E) (nat)) 
    ] 

    [ 
    (types E (nat)) 
    -------------------------- "T-pred" 
    (types (ppred E) (nat)) 
    ] 

    [ 
    (types E (nat)) 
    -------------------------- "T-iszero" 
    (types (iszero E) (bool)) 
    ] 

    [ 
    (types E_1 (bool)) 
    (types E_2 T_1) 
    (types E_3 T_1) 
    -------------------------- "T-iff" 
    (types (iff E_1 E_2 E_3) (T_1)) 
    ] 
) 

据我所知，我们需要使用评估上下文来定义语义。所以我的下一步就是为语言定义这样的上下文和值。

(define-extended-language ty-exp-ctx-val ty-exp 
    (C (suc C) 
    (ppred C) 
    (iszero C) 
    (iff C E E) 
    hole) 
    (NV (zero) 
     (suc NV)) 
    (BV (ttrue) 
     (ffalse)) 
    (V (NV) 
     (BV))) 

非终端C表示上下文，NV为数值，BV为布尔值和V为值。使用值的定义，我定义了一个用于测试表达式是否为值的函数。

(define v? (redex-match ty-exp-ctx-val V)) 

使用该设置，我试图定义该语言操作语义。 在皮尔斯的书，这样的语义（不评价上下文）如下：

e --> e' 
---------------- (E-suc) 
suc e --> suc e' 

------------------ (E-pred-zero) 
pred zero --> zero 

     NV e 
------------------- (E-pred-succ) 
pred (suc e) --> e 

e --> e' 
------------------- (E-pred) 
pred e --> pred e' 


-------------------- (E-iszero-zero) 
iszero zero --> true 

NV e 
------------------------ (E-iszero-succ) 
iszero (suc e) --> false 


e --> e' 
-------------------------(E-iszero) 
iszero e --> iszero e' 

---------------------- (E-if-true) 
if true e e' --> e 

-----------------------(E-if-false) 
if false e e' --> e' 

e --> e' 
-----------------------(E-if) 
if e e1 e2 --> if e' e1 e2 

为了使用评估上下文来表达这样的语义，我删除规则 E-suc，E-pred，E-izero和E-if和步进定义的规则在 表达方面：

e --> e' 
--------------(E-context) 
E[e] --> E[e'] 

据我了解，我们没有必要来表示归约这样的上下文规则。所以， 我已经定义语义这个语言：

(define red 
    (reduction-relation 
    ty-exp-ctx-val 
    #:domain E 
    (--> (in-hole C (iff (ttrue) E_1 E_2)) 
     (in-hole C E_1) 
     "E-if-true") 
    (--> (in-hole C (iff (ffalse) E_1 E_2)) 
     (in-hole C E_2) 
     "E-if-false") 
    (--> (in-hole C (iszero (zero))) 
     (in-hole C (ttrue)) 
     "E-iszero-zero") 
    (--> (in-hole C (iszero (suc (E)))) 
     (in-hole C (ffalse)) 
     (side-condition (v? (term E))) 
     "E-iszero-suc") 
    (--> (in-hole C (ppred (zero))) 
     (in-hole C (zero)) 
     "E-pred-zero") 
    (--> (in-hole C (ppred (suc (E)))) 
     (in-hole C (E)) 
     (side-condition (v? (term E))) 
     "E-pred-suc") 
)) 

现在，我们来的问题：当我试图执行

(traces red (term (iif (iszero zero) ttrue ffalse))) 

球拍返回以下错误信息：

reduction-relation: relation not defined for (iif (iszero (zero)) (ttrue) (ffalse)) 

当然，我正在做一些愚蠢的事情，但我无法弄清楚什么。有人可以帮助我吗？

Answer 1

运行该程序后，我看到了什么问题。

尝试：

(traces red (term (iff (iszero (zero)) (ttrue) (ffalse)))) 

在

(define-language ty-exp 
    [E (ttrue) 
     (ffalse) 
     (zero) 
     (suc E) 
     (ppred E) 
     (iszero E) 
     (iff E E E)] 
    [T (nat) 
    (bool)]) 

你身边ttrue，ffalse和zero括号。