Recbind and Proof Systems
Table of Contents
<expr>::=
| {rebind [<id> : tow = <expr>] <expr>}
Example : {recbind [fact : {num -> num} = {([n : num] => {if {<= n 0}
1
{* n {fact {- n 1}}}})}
{fact 4}]}
given: gama[f->Tow1]|-E1 : tow1....gama[f->tow1]|-E2 :tow2
where: gamma|-{recbind [f : tow 1 = E1] E2} : tow2
1. Interp for recbind
- Create a placeholder for f
- extend the current environment with this place holder
- interp E, in this extended env (call the result V)
- Mutate f in the env/store to V
- Interp E2 in the extended enviornment
2. Proof Systems
p->q
Soundness : If we can prove something, then it is true.
- if type checker proves that code is correct then it should run
q->p
Completeness : If something is true, then we can prove it.
- if your code would have run without type errors then we can run it and it will succedd
- racket is incomplete with casts to tell the typechecker its wrong
can’t have bot of these properties
untyped langauges are complete but not sound