0
$\begingroup$

See this screenshot of the book "Basic Simple Type Theory". The infinite sequence they refer to is just a way to formalize the concept of having enough variables to work with no matter what. In my case, for practical reasons, all my variables are single unicode chars. I forsee for the next 100 years, that to be plenty of mathematical variables to work with.

So I'm in the process of implementing term substitution and I came across this ambiguity in the book:

enter image description here

What do they mean by the last line? Do they mean the first non-free variable including any bound variables within $(N P)$? Or do they mean the first "open, unused, available" variable in all of $(N P)$ including any abstractors $\lambda w$?

My guess is the latter, since $z$ is a dummy variable and of course this can't interfere with other variable useages.

$\endgroup$
  • 1
    $\begingroup$ If I remember correctly, you could without problem have multiple abstractors $\lambda z\cdot( ...\lambda z \cdot ...)$ - they just don't interact with each other. In that case, you can just use the first variable that's not appearing unbound in either $N$ or $P$. Though, if you got enough chars, option #2 of cause can never go wrong $\endgroup$ – Sudix Feb 4 at 21:29
  • $\begingroup$ Thanks @Sudix you are a gentlebeing and a scholar. $\endgroup$ – I Said Roll Up n Smoke Adjoint Feb 4 at 21:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.