Skip to content
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

Merged
merged 10 commits into from
Jan 30, 2024

Conversation

gtrepta
Copy link
Collaborator

@gtrepta gtrepta commented Jan 23, 2024

This replaces the substitution function E[V / X] from the SUBSTITUTION module with manually defined semantics for it in the lambda lessons. It's possible that the SUBSTITUTION module will eventually be dropped from K, so this PR is the beginning of preparation/discovery for making such a change.

Notes:

  • The binder attribute and KVar hooked sort from substitution.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 to a z instead of a y. @ehildenb Is there an alternative option here?
  • The lesson texts are still teaching and referring to the builtin substitution, and need to be rewritten.

Copy link
Contributor

@Scott-Guest Scott-Guest left a 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.

@Baltoli
Copy link
Contributor

Baltoli commented Jan 24, 2024

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.

@gtrepta gtrepta requested a review from Scott-Guest January 29, 2024 20:03
@gtrepta
Copy link
Collaborator Author

gtrepta commented Jan 29, 2024

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.

Copy link
Contributor

@Scott-Guest Scott-Guest left a 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.

@Baltoli
Copy link
Contributor

Baltoli commented Jan 30, 2024

#5

@rv-jenkins rv-jenkins merged commit 0eb060b into master Jan 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants