operational-semantics.rkt (4242B)
1 #lang at-exp s-exp phc-thesis/scribblings/equations-lang 2 3 @; This file is NOT under the CC0 license, as it contains rules and definitions 4 @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the 5 @; permission to copy these rules, but did not ask for a relicensing under the 6 @; CC0 license. 7 8 #:E-Delta 9 10 @$inferrule[@${δ(@primop,@repeated{v}) = v'} 11 @${@app[@primop @repeated{v}] ↪ v'} 12 @${@textsc{E-Delta}}] 13 14 #:E-DeltaE 15 16 @$inferrule[@${@δe(e) = v} 17 @${e ↪ v'} 18 @${@textsc{E-DeltaE}}] 19 20 #:δ-rules 21 22 @$${ 23 \begin{aligned} 24 δ(@textit{add1}, @num-v*{n}) &= @num-v*{n+1} & \\ 25 δ(@textit{number?}, @num-v) &= @true-v & \\ 26 δ(@textit{number?}, v) &= @false-v & @text{otherwise} \\ 27 δ(@consp, v₁, v₂) &= @consv[v₁ v₂] & \\ 28 δ(@textit{car}, @consv[v₁ v₂]) &= v₁ & \\ 29 δ(@textit{cdr}, @consv[v₁ v₂]) &= v₂ & \\ 30 δ(@textit{pair?}, @consv[v v]) &= @true-v & \\ 31 δ(@textit{pair?}, v) &= @false-v & @text{otherwise} \\ 32 δ(@textit{null?}, @null-v) &= @true-v & \\ 33 δ(@textit{null?}, v) &= @false-v & @text{otherwise} \\ 34 δ(@textit{identity}, v) &= v & \\ 35 \end{aligned} 36 } 37 38 #:δe-rules 39 40 @$${ 41 \begin{aligned} 42 @δe(@num-e) = @num-v \\ 43 @δe(@true-e) = @true-v \\ 44 @δe(@false-e) = @false-v \\ 45 @δe(@null-e) = @null-v \\ 46 @δe(@λe[(@repeated{x:τ}) e]) = @λv[(@repeated{x_r:τ}) e] \\ 47 @δe(@λe[(@repeated{x:τ} @${\ .\ } @${x_r:σ*}) e]) 48 = @λv[(@repeated{x:τ} @${\ .\ } @${x:σ*}) e] \\ 49 @δe(@λe[(@repeated{x:τ} @${\ .\ } @${x_r:@polydot[σ α]}) e]) 50 = @λv[(@repeated{x:τ} @${\ .\ } @${x_r:@polydot[σ α]}) e] \\ 51 @δe(@Λe[(@repeated{α}) e]) = @Λv[(@repeated{α}) e] \\ 52 @δe(@Λe[(@repeated{α} @polydotα[β]) e]) = @Λv[(@repeated{α} @polydotα[β]) e] \\ 53 @δe(@promisee[e]) = @promisev[e] \\ 54 @δe(@syme[s]) = @symv[s] 55 \end{aligned} 56 } 57 58 #:E-Beta 59 60 @$inferrule[- 61 @${@app[@λv[(@repeated{x:τ}) e_b] @repeated{e_a}] 62 ↪ e_b@subst[@repeated{x ↦ e_a}]} 63 @${@textsc{E-Beta}}] 64 65 #:E-Beta* 66 67 @$inferrule[- 68 @${ 69 @app[@λv[(@repeated[#:n "n"]{x:τ} @${\ .\ } @${x_r:τ_r*}) e_b] 70 @repeated[#:n "n"]{e_a} @repeated[#:n "m"]{e_r}] 71 ↪ e_b@subst[x_r ↦ @listv[@repeated[#:n "m"]{e_r}] 72 @repeated[#:n "n"]{x ↦ e_a}]} 73 @${@textsc{E-Beta*}}] 74 75 #:E-BetaD 76 77 @$inferrule[- 78 @${ 79 @app[@λv[(@repeated[#:n "n"]{x:τ} @${\ .\ } 80 @${x_r:@polydot[τ_r α]}) e_b] 81 @repeated[#:n "n"]{e_a} @repeated[#:n "m"]{e_r}] 82 ↪ e_b@subst[x_r ↦ @listv[@repeated[#:n "m"]{e_r}] 83 @repeated[#:n "n"]{x ↦ e_a}]} 84 @${@textsc{E-BetaD}}] 85 86 #:E-TBeta 87 88 @$inferrule[- 89 @${@at[@Λv[(@repeated{α}) e] @repeated{τ}] ↪ e} 90 @${@textsc{E-TBeta}}] 91 92 #:E-TDBeta 93 94 @$inferrule[- 95 @${@at[@Λv[(@repeated{α} @polydotα[β]) e] @repeated{τ}] ↪ e} 96 @${@textsc{E-TDBeta}}] 97 98 @λe[(@repeated{x:τ} @${\ .\ } @${x:τ*}) e] 99 100 #:E-If-False 101 102 @$inferrule[- 103 @${@ifop[@false-v e₂ e₃] ↪ e₃} 104 @${@textsc{E-If-False}}] 105 106 #:E-If-True 107 108 @$inferrule[@${v ≠ @false-v} 109 @${@ifop[v e₂ e₃] ↪ e₃} 110 @${@textsc{E-If-True}}] 111 112 #:E-Force 113 114 @$inferrule[@${e ↪ v} 115 @${@forcee[@promisev[e]] ↪ v} 116 @${@textsc{E-Force}}] 117 118 #:E-Gensym 119 120 @$inferrule[@${v = @sym* @text{ fresh}} 121 @${@gensyme[] ↪ v} 122 @${@textsc{E-Gensym}}] 123 124 #:E-Eq?-True 125 126 @$inferrule[@${v₁ = v₂} 127 @${@eq?op[v₁ v₂] ↪ @true-v} 128 @${@textsc{E-Eq?-True}}] 129 130 #:E-Eq?-False 131 132 @$inferrule[@${v₁ ≠ v₂} 133 @${@eq?op[v₁ v₂] ↪ @false-v} 134 @${@textsc{E-Eq?-False}}] 135 136 #:E-Map-Pair 137 138 @$inferrule[@${} 139 @${@mapop[v_f @consv[v₁ v₂]] ↪ @consp[@app[v_f v₁] @mapop[v_f v₂]]} 140 @${@textsc{E-Map-Pair}}] 141 142 #:E-Map-Null 143 144 @$inferrule[@${} 145 @${@mapop[v_f @null-v] ↪ @null-v} 146 @${@textsc{E-Map-Null}}] 147 148 #:E-Context 149 150 ;; TODO: check what this means (and is it the right kind of arrow?) 151 @$inferrule[@${L ↪ R} 152 @${E[L] ↪ E[R]} 153 @${@textsc{E-Context}}]