A Binding Calculation
John Power – 1 May 2024
A few years ago, I gave two talks on Miki Tanaka and my generalisation of Plotto et al's 1999 work on variable binding. It inherently involves a definition of binding signature. At the end of my second talk, Steve asked whether there is a natural mathematical reason for the definition as stated. I could not answer then, and I still cannot. However, although I stated the key theorem that a binding signature must satisfy, I did not explain the proof, which I regarded, and still regard, as remarkably delicate. So I propose to give a little background in order to make the motivation for the calculation somewhat comprehensible, then try to explain the proof. My hope is that one of you, or I, might see a more conceptual formulation of binding signature that reflects the theorem. Nobody other than Marcelo Fiore seems to have done much with Plotto et al's work, but I think it was fine work that merits thought.
Back