This thesis studies two major extensions of nominal terms. In particular, we study an extension with lambda abstraction over nominal unknowns and atoms, and an extension with an arguably better theory of freshness and alpha-equivalence. Nominal terms possess two levels of variable: atoms a represent variable symbols, and unknowns X are 'real' variables. As a syntax, they are designed to facilitate metaprogramming; unknowns are used to program on syntax with variable symbols. Originally, the role of nominal terms was interpreted narrowly. That is, they were seen solely as a syntax for representing partially-specified abstract syntax with binding.
The main motivation of this thesis is to extend nominal terms so that they can be used for metaprogramming on proofs, programs, etc. and not just for metapro- gramming on abstract syntax with binding. We therefore extend nominal terms in two significant ways: adding lambda abstraction over nominal unknowns and atoms facilitating functional programing and improving the theory of alpha-equivalence that nominal terms possesses.
Neither of the two extensions considered are trivial. The capturing substitution action of nominal unknowns implies that our notions of scope, intuited from working with syntax possessing a non-capturing substitution, such as the lambda calculus, is no longer applicable. As a result, notions of lambda abstraction and alpha-equivalence must be carefully reconsidered.
In particular, the first research contribution of this thesis is the two-level lambda calculus, intuitively an intertwined pair of lambda calculi. As the name suggests, the two-level lambda calculus has two level of variable, modelled by nominal atoms and un- knowns, respectively. Both levels of variable can be lambda abstracted, and requisite notions of beta-reduction are provided. The result is an expressive context-calculus. The traditional problems of handling alpha-equivalence and the failure of commutation between instantiation and beta-reduction in context-calculi are handled through the use of two distinct levels of variable, swappings, and freshness side-conditions on unknowns, i.e. 'nominal technology'.
The second research contribution of this thesis is permissive nominal terms, an alternative form of nominal term. They retain the 'nominal' first-order flavour of nominal terms (in fact, their grammars are almost identical) but forego the use of explicit freshness contexts. Instead, permissive nominal terms label unknowns with a permission sort, where permission sorts are infinite and coinfinite sets of atoms. This infinite-coinfinite nature means that permissive nominal terms recover two properties we call them the 'always-fresh' and 'always-rename' properties that nominal terms lack. We argue that these two properties bring the theory of alpha-equivalence on permissive nominal terms closer to 'informal practice'.
The reader may consider lambda abstraction and alpha-equivalence so familiar as to be 'solved problems'. The work embodied in this thesis stands testament to the fact that this isn't the case. Considering lambda abstraction and alpha-equivalence in the context of two levels of variable poses some new and interesting problems and throws light on some deep questions related to scope and binding.