Dan's 數位πŸͺ΄εœ’

Can Naive substitution work if all variables has different name?

1 min read

First counter example

(πœ†π‘₯.πœ†π‘¦.π‘₯)𝑦=πœ†π‘¦.𝑦

but this is an open term, right y is a free variable.

counter example without free variable

From: https://hachyderm.io/@LordQuaggan/113894693329581835

(πœ†π‘“.𝑓𝑓)(πœ†π‘₯.πœ†π‘¦.π‘₯𝑦)=(πœ†π‘₯.πœ†π‘¦.π‘₯𝑦)(πœ†π‘₯.πœ†π‘¦.π‘₯𝑦)=πœ†π‘¦.((πœ†π‘₯.πœ†π‘¦.π‘₯𝑦)𝑦)=πœ†π‘¦.(πœ†π‘¦.𝑦𝑦)
  • ζ³¨ζ„εˆ° y εˆ†εˆ₯θ¦εƒη…§ζœ€ε€–ηš„θˆ‡ζœ€ε…§ηš„

advanced question: can binding as sets of scopes solve this problem?

Yes, but this is slower than usual algorithm.

Graph View