-
Notifications
You must be signed in to change notification settings - Fork 2
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Replace uses of builtin substitution with custom semantics for lambda #3
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We could fix the variable capture issue by manually alpha converting when necessary:
// Produce a fresh var which does not occur in the set
syntax Id ::= freshFrom(Set) [function]
rule freshFrom(S) => #if !I:Id in S #then freshFrom(S) #else I #fi
// Collect all the free variables in a term
syntax Set ::= freeVars(Exp) [function]
rule (lambda X . E) [_ / X] => lambda X . E
rule (lambda X . E) [V / Y] => lambda X . (E [V / Y]) requires (X =/=K Y) andBool (notBool (X in freeVars(V)))
rule (lambda X . E) [V / Y] => #let Z = freshFrom(freeVars(V) freeVars(E)) #in (lambda Z . (E [Z / X] [V / Y])) [owise]
Alternatively, we could use DeBruijn indices or a locally nameless representation. This might be conceptually clearer, but would require converting between the program syntax and the internal representation using these indices.
Indeed; the "pure K" solution implemented here will need a way of dealing with alpha-conversion. I think for the purposes of this language, we can do so explicitly rather than implementing locally nameless / de bruijn indices etc. |
I've updated this to use custom semantics for alpha conversion. Note that I haven't updated lesson documentation yet because we can revert this back to using the substitution module if we implement the frontend pass to generate these semantics. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM. I'd open an issue to note that we still have to update the documentation.
This replaces the substitution function
E[V / X]
from theSUBSTITUTION
module with manually defined semantics for it in the lambda lessons. It's possible that theSUBSTITUTION
module will eventually be dropped from K, so this PR is the beginning of preparation/discovery for making such a change.Notes:
binder
attribute andKVar
hooked sort fromsubstitution.md
is still being used for renaming variables that have duplicate names. Without them, then the free variable capture example (a (((lambda x.lambda y.x) y) z)
) will evaluate incorrectly toa z
instead ofa y
. @ehildenb Is there an alternative option here?