[PRL] fresh variables in call/cc

Matthias Felleisen matthias at ccs.neu.edu
Mon Mar 12 10:38:27 EDT 2007


You don't need the freshness condition for this language. -- Matthias


On Mar 12, 2007, at 10:28 AM, Dave Herman wrote:

> IIRC, a common way to specify call/cc operationally is by turning the
> captured continuation back into an ordinary expression:
>
>      e ::= x | \x.e | (e e) | (call/cc e) | (abort e)
>      v ::= \x.e
>      E ::= [] | (E e) | (v E)
>
>      E[\x.e v]    -> E[e[v/x]]
>      E[call/cc v] -> E[v[\z.abort(E[z])]]  (z fresh w.r.t. E)
>      E[abort e]   -> e
>
> Is the freshness condition necessary for the call/cc rule? It looked
> "obvious" to me, since you don't want the variable representing the  
> hole
> to be captured, but I can't see *how* it could be captured. AFAICT,  
> you
> can't put the hole under a binder in this language, and rightly so; we
> don't evaluate under binders. (After all, to quote Olin, "binders
> dominate references.")
>
> Dave
>
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl




More information about the PRL mailing list