trules.rkt (12468B)
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 @(define _op @${_{\mathit{op}}}) 9 10 #: 11 12 #:T-Promise 13 14 @$inferrule[@${@Γ[⊢ e @R[τ φ⁺ φ⁻ o]]} 15 @${@Γ[⊢ @promisee[e] @R[@promiseτ[@R[τ φ⁺ φ⁻ o]] ϵ ⊥ ∅]]} 16 @${@textsc{T-Promise}}] 17 18 #:T-Symbol 19 20 @$inferrule[- 21 @${@Γ[⊢ @syme[s] @R[@symτ[s] ϵ ⊥ ∅]]} 22 @${@textsc{T-Symbol}}] 23 24 #:T-Gensym 25 26 @$inferrule[- 27 @${@Γ[⊢ @gensyme[] @R[@Symbolτ ϵ ⊥ ∅]]} 28 @${@textsc{T-Gensym}}] 29 30 #:T-Eq? 31 32 @$inferrule[@${@Γ[⊢ e₁ @R[τ₁ φ⁺₁ φ⁻₁ o₂]] \\ 33 @Γ[⊢ e₂ @R[τ₂ φ⁺₂ φ⁻₂ o₂]] \\ 34 @<:[τ₁ @Symbolτ] \\ 35 @<:[τ₂ @Symbolτ]} 36 @${@Γ[⊢ @eq?op[e₁ e₂] @R[@Booleanτ ϵ ⊥ ∅]]} 37 @${@textsc{T-Eq}\mathrm{?}}] 38 39 #:T-Var 40 41 @$inferrule[- 42 @${@Γ[⊢ x @R[@${Γ(x)} @${@!{@false-τ}} @true-τ x]]} 43 @${@textsc{T-Var}}] 44 45 #:T-Primop 46 47 @$inferrule[- 48 @${@Γ[⊢ p @R[@${δ_τ(p)} ϵ ⊥ ∅]]} 49 @${@textsc{T-Primop}}] 50 51 #:T-True 52 53 @$inferrule[- 54 @${@Γ[⊢ @true-e @R[@true-τ ϵ ⊥ ∅]]} 55 @${@textsc{T-True}}] 56 57 #:T-False 58 59 @$inferrule[- 60 @${@Γ[⊢ @false-e @R[@false-τ ⊥ ϵ ∅]]} 61 @${@textsc{T-False}}] 62 63 #:T-Num 64 65 @$inferrule[- 66 @${@Γ[⊢ @num-e @R[@num-τ ϵ ⊥ ∅]]} 67 @${@textsc{T-Num}}] 68 69 #:T-Null 70 71 @$inferrule[- 72 @${@Γ[⊢ @null-e @R[@null-τ ⊥ ϵ ∅]]} 73 @${@textsc{T-Null}}] 74 75 #:T-DMap 76 77 @$inferrule[@${@Γ[⊢ e_r @R[@polydot[τ_r α] φ⁺_r φ⁻_r o_r]] \\ 78 @Γ[⊢ e_f @R[@∀r[(β) @f→[(@${τ_r@subst[α ↦ β]}) @R[τ φ⁺ φ⁻ o]]] 79 φ⁺_f 80 φ⁻_f 81 o_f]]} 82 @${@Γ[⊢ @mapop[e_f e_r] @R[@polydot[@${τ@subst[β ↦ α]} α] 83 ϵ 84 ⊥ 85 ∅]]} 86 @${@textsc{T-DMap}}] 87 88 #:T-AbsPred 89 90 @$inferrule[@${@Γ[@${x₀:σ₀} @repeated{xᵢ:σᵢ} ⊢ e @R[τ φ⁺ φ⁻ o]] \\ 91 φ⁺' = φ⁺\vphantom{φ}@substφo[x₀ ↦ •] \\ 92 φ⁻' = φ⁻\vphantom{φ}@substφo[x₀ ↦ •] \\ 93 o' = o\vphantom{o}@substφo[x₀ ↦ •]} 94 @${@Γ[⊢ @λe[(x₀:σ₀ @repeated{xᵢ:σᵢ}) e] 95 @R[(f→ (@repeated{σ}) 96 @R[τ 97 @${φ⁺'} 98 @${φ⁻'} 99 @${o'}]) 100 ϵ ⊥ ∅]]} 101 @${@textsc{T-AbsPred}}] 102 103 #:T-Abs 104 105 @$inferrule[@${@Γ[@repeated{x:σ} ⊢ e @R[τ φ⁺ φ⁻ o]]} 106 @${@Γ[⊢ @λe[(@repeated{x:σ}) e] 107 @R[(f→ (@repeated{σ}) 108 @R[τ 109 ϵ 110 ϵ 111 ∅]) 112 ϵ ⊥ ∅]]} 113 @${@textsc{T-Abs}}] 114 115 #:T-Abs* 116 117 @$inferrule[@${@Γ[@repeated{x:σ} @${x_r:@Listofτ[σ_r]} ⊢ e @R[τ φ⁺ φ⁻ o]]} 118 @${@Γ[⊢ @λe[(@repeated{x:σ} @${\ .\ } @${x_r:σ_r*}) e] 119 @R[(f* (@repeated{σ} σ_r) 120 @R[τ 121 ϵ 122 ϵ 123 ∅]) 124 ϵ ⊥ ∅]]} 125 @${@textsc{T-Abs*}}] 126 127 #:T-DAbs 128 129 @$inferrule[@${@repeated{Δ ⊢ τₖ} \\ 130 Δ ▷ @polydot[τ_r α] \\ 131 @Γ[@repeated{xₖ : τₖ} @${x_r : @polydot[τ_r α]} ⊢ e @R[τ φ⁺ φ⁻ o]]} 132 @${@Γ[⊢ @λe[(@repeated{xₖ:τₖ} @${x_r:@polydot[τ_r α]}) e] 133 @R[(f… (@repeated{τₖ} @polydot[τ_r α]) 134 @R[τ 135 ϵ 136 ϵ 137 ∅]) 138 ϵ ⊥ ∅]]} 139 #:wide #t 140 @${@textsc{T-DAbs}}] 141 142 #:T-TAbs 143 144 @$inferrule[@${@Γ[Δ @${\{@repeatset{α}\}} ⊢ e @R[τ φ⁺ φ⁻ o]]} 145 @${@Γ[⊢ @Λe[(@repeated{α}) e] 146 @R[(∀r (@repeated{α}) 147 @R[τ 148 ϵ 149 ϵ 150 ∅]) 151 ϵ ⊥ ∅]]} 152 @${@textsc{T-TAbs}}] 153 154 #:T-DTAbs 155 156 @$inferrule[@${@Γ[Δ @${\{@repeatset{α}\}} @${\{@polydotα{β}\}} 157 ⊢ e @R[τ φ⁺ φ⁻ o]]} 158 @${@Γ[⊢ @Λe[(@repeated{α} @polydotα{β}) e] 159 @R[(∀r (@repeated{α} @polydotα{β}) 160 @R[τ 161 ϵ 162 ϵ 163 ∅]) 164 ϵ ⊥ ∅]]} 165 @${@textsc{T-DTAbs}}] 166 167 #:substφ 168 169 @$${ 170 \begin{aligned} 171 φ@substφo[x ↦ z] &= \bigcup @repeated{ψ@substφo[x ↦ z]}&\\ 172 ⊥@substφo[x ↦ z] &= \{⊥\}&\\ 173 τ_{π(y)}\vphantom{τ}@substφo[x ↦ z] &= ∅ &@textif y ≠ x \\ 174 @!{τ}_{π(y)}\vphantom{τ}@substφo[x ↦ z] &= ∅ &@textif y ≠ x \\ 175 τ_{π(x)}\vphantom{τ}@substφo[x ↦ z] &= \{τ_{π(z)}\} &\\ 176 @!{τ}_{π(x)}\vphantom{τ}@substφo[x ↦ z] &= \{@!{τ}_{π(z)}\} & 177 \end{aligned} 178 } 179 180 #:substo 181 182 @$${ 183 \begin{aligned} 184 π(x)@substφo[x ↦ ∅] &= ∅ &\\ 185 π(x)@substφo[x ↦ z] &= π(z) &@textif z ≠ ∅ \\ 186 π(y)@substφo[x ↦ z] &= ∅ &@textif y ≠ x \\ 187 ∅@substφo[x ↦ z] &= ∅ & 188 \end{aligned} 189 } 190 191 #:T-App 192 193 @$inferrule[@${@Γ[⊢ @${e@_op} @R[@${τ@_op} @${φ⁺@_op} @${φ⁻@_op} @${o@_op}]] \\ 194 @repeated[@Γ[⊢ @${aᵢ} 195 @R[@${τ_{aᵢ}} @${φ⁺_{aᵢ}} @${φ⁻_{aᵢ}} @${o_{aᵢ}}]]] \\ 196 @repeated[@<:[τ_a @${τ_{\mathit{in}}}]] 197 @<:[@${τ@_op} @f→[(@repeated{τ_{\mathit{in}}}) 198 @R[τ_r φ⁺_r φ⁻_r o_r]]] \\ 199 φ⁺_r' = φ⁺_r@substφo[• ↦ @${o_{a_0}}] \\ 200 φ⁻_r' = φ⁻_r@substφo[• ↦ @${o_{a_0}}] \\ 201 o' = o@substφo[• ↦ @${o_{a_0}}]} 202 @${@Γ[⊢ @app[@${e@_op} @repeated{aᵢ}] 203 @R[(f→ (@repeated{σ}) 204 @R[τ_r 205 @${φ⁺'} 206 @${φ⁻'} 207 @${o'}]) 208 ϵ ⊥ ∅]]} 209 #:wide 'latex 210 @${@textsc{T-App}}] 211 212 #:T-Inst 213 214 @$inferrule[@${@repeated{Δ ⊢ τⱼ} \\ 215 @Γ[⊢ @${e@_op} @R[@∀r[(@repeated{αⱼ}) τ] φ⁺ φ⁻ o]]} 216 @Γ[⊢ @at[@${e@_op} @repeated{τⱼ}] 217 @R[@${τ@subst[@repeated{aⱼ ↦ τⱼ}]} 218 ϵ ϵ ∅]] 219 @${@textsc{T-Inst}}] 220 221 #:T-DInst 222 223 @$inferrule[@${@repeated[#:n "n"]{Δ ⊢ τⱼ} \\ 224 @repeated[#:n "m"]{Δ ⊢ τₖ} \\ 225 @Γ[⊢ @${e@_op} @R[@∀r[(@repeated[#:n "n"]{αⱼ} @polydotα[β]) τ] 226 φ⁺ φ⁻ o]]} 227 @Γ[⊢ @at[@${e@_op} @repeated[#:n "n"]{τⱼ} @repeated[#:n "m"]{τₖ}] 228 @R[@transdots[@${τ@subst[@repeated[#:n "n"]{aⱼ ↦ τⱼ}]} 229 @${β} 230 @repeated[#:n "m"]{τₖ}] 231 ϵ ϵ ∅]] 232 @${@textsc{T-DInst}}] 233 234 #:T-DInstD 235 236 @$inferrule[@${@repeated{Δ ⊢ τₖ} \\ 237 Δ ▷ @polydot[τ_r β] \\ 238 @Γ[⊢ @${e@_op} @R[@∀r[(@repeated{αₖ} @polydotα[α_r]) τ] 239 φ⁺ φ⁻ o]]} 240 @Γ[⊢ @at[@${e@_op} @repeated{τₖ} @polydot[τ_r β]] 241 @R[@substdots[@${τ@subst[@repeated{aₖ ↦ τₖ}]} 242 @${α_r} 243 @${τ_r} 244 @${β}] 245 ϵ ϵ ∅]] 246 @${@textsc{T-DInstD}}] 247 248 #:T-If 249 250 @$inferrule[@${@Γ[⊢ @${e₁} @R[@${τ₁} @${φ⁺₁} @${φ⁻₁} @${o₁}]] \\ 251 @Γ[+ φ⁺₁ ⊢ @${e₂} @R[@${τ₂} @${φ⁺₂} @${φ⁻₂} @${o₂}]] \\ 252 @Γ[+ φ⁻₁ ⊢ @${e₃} @R[@${τ₃} @${φ⁺₃} @${φ⁻₃} @${o₃}]] \\ 253 @<:[τ₂ τ_r] \\ 254 @<:[τ₃ τ_r] \\ 255 φ_r⁺ / φ_r⁻ = @combinefilter(φ⁺₁ / φ⁻₁, φ⁺₂ / φ⁻₂, φ⁺₃ / φ⁻₃) \\ 256 o_r = \begin{cases} 257 o₂ @& @textif o₂ = o₃ 258 @nl ∅ @& @otherwise 259 \end{cases}} 260 @${@Γ[⊢ @ifop[e₁ e₂ e₃] @R[τ_r φ_r⁺ φ_r⁻ o_r]]} 261 #:wide 'latex 262 @${@textsc{T-If}}] 263 264 #:Γ+ 265 266 @aligned{ 267 Γ + \{τ_{π(x)}\} ∪ @repeatset{ψ} 268 &= (Γ, x : @update(Γ(x), τ_π)) + @repeatset{ψ}\\ 269 Γ + \{@!{τ}_{π(x)}\} ∪ @repeatset{ψ} 270 &= (Γ, x : @update(Γ(x), @!{τ}_π)) + @repeatset{ψ}\\ 271 Γ + \{⊥\} ∪ @repeatset{ψ} &= Γ' 272 @where ∀x∈ \operatorname{dom}(Γ).@=:[@${Γ'(x)} ⊥]\\ 273 Γ + ϵ &= Γ \\ 274 } 275 276 #:update 277 278 @aligned{ 279 @update(@consτ[τ τ′], σ_{π∷car} ) 280 &= @consτ[@${@update(τ, σ_π)} τ′]\\ 281 @update(@consτ[τ τ′], @!{σ}_{π∷car}) 282 &= @consτ[@${@update(τ, @!{σ}_π)} τ′]\\ 283 @update(@consτ[τ τ′], σ_{π∷cdr} ) 284 &= @consτ[τ @${@update(τ′, σ_π)}]\\ 285 @update(@consτ[τ τ′], @!{σ}_{π∷cdr} ) 286 &= @consτ[τ @${@update(τ′, @!{σ}_π)}]\\ 287 @update(τ, σ_ϵ) &= @restrict(τ, σ) \\ 288 @update(τ, @!{σ}_ϵ) &= @remove(τ, σ) 289 } 290 291 #:restrict 292 293 @aligned{ 294 @restrict(τ, σ) &= ⊥ &@textif @no-overlap(τ,σ)\\ 295 @restrict(@un[@repeatset{τ}], σ) &= @un[@repeatset{@restrict(τ,σ)}] &\\ 296 @restrict(τ, σ) &= τ &@textif @<:[τ σ]\\ 297 @restrict(τ, σ) &= σ &@otherwise 298 } 299 300 #:remove 301 302 @aligned{ 303 @remove(τ, σ) &= ⊥ &@textif @<:[τ σ] \\ 304 @remove(@un[@repeatset{τ}], σ) &= @un[@repeatset{@remove(τ,σ)}] &\\ 305 @remove(τ, σ) &= τ &@otherwise 306 } 307 308 #:no-overlap 309 310 @aligned{ 311 @no-overlap(τ, τ′) &= @metatrue 312 &&@textif ∄ σ .\begin{aligned}[t] 313 &@<:[σ τ]\\ 314 {}\mathbin{∧}{} &@<:[σ τ′]\\ 315 {}\mathbin{∧}{} &Δ ⊢ σ\\ 316 {}\mathbin{∧}{} &@≠:[σ ⊥]\end{aligned}\\ 317 @no-overlap(τ, σ) &= @metafalse 318 &&@otherwise 319 } 320 321 @;{ 322 @aligned{ 323 @no-overlap(@num-τ[n], @num-τ[m]) &= @metatrue @textif n ≠ m \\ 324 @no-overlap(@num-τ, @true-τ) &= @metatrue \\ 325 @no-overlap(@num-τ, @false-τ) &= @metatrue \\ 326 @no-overlap(@num-τ, @null-τ) &= @metatrue \\ 327 @no-overlap(@Numberτ, @true-τ) &= @metatrue \\ 328 @no-overlap(@Numberτ, @false-τ) &= @metatrue \\ 329 @no-overlap(@Numberτ, @null-τ) &= @metatrue \\ 330 @no-overlap(@true-τ, @false-τ) &= @metatrue \\ 331 @no-overlap(@true-τ, @null-τ) &= @metatrue \\ 332 @no-overlap(@false-τ, @null-τ) &= @metatrue \\ 333 @no-overlap(@num-τ, @f→[(@repeated{τ}) @R]) &= @metatrue \\ 334 @no-overlap(@Numberτ, @f→[(@repeated{τ}) @R]) &= @metatrue \\ 335 @no-overlap(@true-τ, @f→[(@repeated{τ}) @R]) &= @metatrue \\ 336 @no-overlap(@false-τ, @f→[(@repeated{τ}) @R]) &= @metatrue \\ 337 @no-overlap(@consτ[τ τ′], @f→[(@repeated{τ}) @R]) &= @metatrue \\ 338 @no-overlap(@null-τ, @f→[(@repeated{τ}) @R]) &= @metatrue \\ 339 @no-overlap(@num-τ, @consτ[τ τ′]) &= @metatrue \\ 340 @no-overlap(@Numberτ, @consτ[τ τ′]) &= @metatrue \\ 341 @no-overlap(@true-τ, @consτ[τ τ′]) &= @metatrue \\ 342 @no-overlap(@false-τ, @consτ[τ τ′]) &= @metatrue \\ 343 @no-overlap(@null-τ, @consτ[τ τ′]) &= @metatrue \\ 344 @no-overlap(@consτ[τ τ′], @consτ[σ σ′]) 345 &= @no-overlap(τ,σ) ∨ @no-overlap(τ′,σ′)\\ 346 @no-overlap((⋃ @repeatset{τ}), σ) &= ⋀@repeated{@no-overlap(τ,σ)}\\ 347 @no-overlap(τ, σ) &= @metatrue @textif @no-overlap(σ, τ)\\ 348 @no-overlap(τ, σ) &= @metafalse @otherwise \\ 349 } 350 } 351 352 #:combinefilter 353 354 @aligned{ 355 @combinefilter(ϵ / ⊥, φ^±₂, φ^±₃) &= φ^±₂ \\ 356 @combinefilter(⊥ / ϵ, φ^±₂, φ^±₃) &= φ^±₃ \\ 357 @combinefilter(⊥ / ⊥, φ^±₂, φ^±₃) &= ⊥ &\\ 358 @combinefilter(φ⁺₁ / φ⁻₁, φ⁺₂ / φ⁻₂, ⊥/ϵ) &= φ⁺₁ ∪ φ⁺₂ \\ 359 @combinefilter( 360 \{ τ_{π(@loc)} \} ∪ φ⁺₁ / \{ @!{τ}_{π(@loc)} \} φ⁻₁, 361 ϵ / ⊥, 362 ⊥/ϵ) 363 &= (∪\ τ\ σ)_{π(@loc)} / @!{(∪\ τ\ σ)_{π(@loc)}} \\ 364 … & = … & \\ 365 @combinefilter(φ^±₁, φ^±₂, φ^±₃) &= ϵ / ϵ \qquad @otherwise \\ 366 }