You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Note from Ian:
"The possible questions on the alpha-conversion are to do with you having an implementation working almost entirely at the top level, rather than recursively down the structure of terms. All of the detailed operations are done recursively, of course --- free names, bound names, renaming --- but the strategy for capture avoidance is to call each of those from the top level, rather than, say, define capture-avoiding renaming directly by recursion. I think it's safe, but there are some curiosities. For example, when a name appears in a term both bound and free, in different subterms."
The text was updated successfully, but these errors were encountered:
Capture avoiding substitution needs redefining.
Note from Ian:
"The possible questions on the alpha-conversion are to do with you having an implementation working almost entirely at the top level, rather than recursively down the structure of terms. All of the detailed operations are done recursively, of course --- free names, bound names, renaming --- but the strategy for capture avoidance is to call each of those from the top level, rather than, say, define capture-avoiding renaming directly by recursion. I think it's safe, but there are some curiosities. For example, when a name appears in a term both bound and free, in different subterms."
The text was updated successfully, but these errors were encountered: