–
Room P3.10, Mathematics Building
Metaprogramming is programming on syntax, as we do to implement lambda-calculus reduction, or proof-search in a sequent logic. We bind names with lambda and generate eigenvariables with forall introduction in the two examples above. The usual notion of syntax is "abstract syntax tree" but this provide an unsatisfactory abstract model of these phenomena. There is a need for a notion of "abstract syntax tree" in which variable names may be literally bound and generated, in some suitable mathematical sense. I shall present Fraenkel-Mostowski (FM) sets, which is ZFA set theory (ZF set theory with atoms) with one extra axiom. I shall show how this set theory sustains an improved model of syntax in which binding and name-generation are set-theoretic phenomena whose application to sets representing abstract syntax trees coincides with our usual concrete constructions on syntax. I will conclude with a brief discussion of the significance of this discovery for programming and logic.