Ancestors

Written by Zhixuan Yang on 2025-01-26 at 00:56

Can I ask a question as an absolutely novice language implementor? Suppose I want to implement a substitution-based evaluator of some language. After parsing a term into a syntax tree, can I just rename binders in the program to make sure no binders use the same variable name, and then

just forget about capture avoidance when substituting?

(As for why I am doing this: I am playing with a representation of free monads that has amortised constant-time-per-variable substitution and constant-time case analysis, so I'd like to see how fast a stupid evaluator can be if the underlying data structure is clever)

=> More informations about this toot | More toots from zyang@mathstodon.xyz

Written by Andreas Nuyts on 2025-01-26 at 01:03

@zyang I'd say not unless your language enforces linear or affine usage of variables.

As soon as a variable is used twice, substitution will not respect the intended invariant that no two binders use the same variable name.

=> More informations about this toot | More toots from anuytstt@fosstodon.org

Written by Lîm Tsú-thuàn on 2025-01-26 at 05:09

@anuytstt @zyang Do you have an example?

=> More informations about this toot | More toots from dannypsnl@g0v.social

Written by Zhixuan Yang on 2025-01-26 at 10:27

@dannypsnl @anuytstt Good question! To actually construct an example of normalising an all-binder-distinct λ-term using reckless substitution goes wrong, we need to construct a λ-term t such that t has no binders sharing the same variable, and by a sequence of reckless β-reduction t ->* λy. ... (λx. ... λ y. ... x ...) y), which looks like a good Sunday puzzle for me.

=> More informations about this toot | More toots from zyang@mathstodon.xyz

Written by Lîm Tsú-thuàn on 2025-01-26 at 11:09

@zyang @anuytstt For free variables occurs at initial term, I already see it can fail, e.g.

(\x. \y. x) y = \y. y (oops)

so if we disallow free variables (all are bound now), then?

=> More informations about this toot | More toots from dannypsnl@g0v.social

Toot

Written by Zhixuan Yang on 2025-01-26 at 12:18

@dannypsnl yep, I haven't got an example yet. (But mostly because I have been only watching youtube today 😅 )

=> More informations about this toot | More toots from zyang@mathstodon.xyz

Descendants

Written by Nathaniel Burke on 2025-01-26 at 12:38

@zyang @dannypsnl

(\f. f f) (\x y. x y)

->

(\x y. x y) (\x y. x y)

->

(\y. (\x y. x y) y)

->

(\y. (\y. y y))

=> More informations about this toot | More toots from LordQuaggan@hachyderm.io

Written by Zhixuan Yang on 2025-01-26 at 12:41

@LordQuaggan @dannypsnl Amazing, thanks!

=> More informations about this toot | More toots from zyang@mathstodon.xyz