deltarules.rkt (1607B)
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 @$${ 9 \begin{aligned} 10 δ(@textit{add1}) = 11 @f→[(Numberτ) @R[Numberτ ϵ ⊥ ∅]] \\ 12 δ(@textit{number?}) = 13 @f→[(⊤) @R[Boolean @${@|Numberτ|_•} @${@![Numberτ]_•} ∅]] \\ 14 δ(@textit{pair?}) = 15 @f→[(⊤) @R[Boolean @${@consτ[⊤ ⊤]_•} @${@![@consτ[⊤ ⊤]]_•} ∅]] \\ 16 δ(@textit{null?}) = 17 @f→[(⊤) @R[Boolean @${@|null-τ|_•} @${@![null-τ]_•} ∅]] \\ 18 δ(@textit{identity}) = @∀r[(α) @f→[(α) @R[α 19 @${@![false-v]_{•}} 20 @${@|false-v|_{•}} 21 @${•}]]] \\ 22 δ(@consp) = @∀r[(α β) @f→[(α β) @R[@consτ[α β] ϵ ⊥ ∅]]] \\ 23 δ(@textit{car}) = @∀r[(α β) @f→[(@consτ[α β]) @R[α 24 @${@![false-v]_{car(•)}} 25 @${@|false-v|_{car(•)}} 26 @${car(•)}]]] \\ 27 δ(@textit{cdr}) = @∀r[(α β) @f→[(@consτ[α β]) @R[β 28 @${@![false-v]_{cdr(•)}} 29 @${@|false-v|_{cdr(•)}} 30 @${cdr(•)}]]] \\ 31 \end{aligned} 32 }