[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