redexで小さな言語を定義しようとしています

Question

私は、Redex用にamb tutorialに従うと同時に、Pierceのタイプとプログラミング言語にある型付き算術式のモデルを構築しています。

私はこのような小さな言語の構文と型システムを定義しましたが、小さなステップセマンティクスを定義するのは難しいです。私が問題になる前に、私がこれまでに得た定義を提示しましょう。

まず、言語の構文を定義しました。

(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

プログラムを実行した後、私は問題が何かを確認します。

試してみてください。

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

で

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

あなたがttrue、ffalseとzero周りに括弧を持っています。