GFOL: a Term-Generic Logic for Defining Lambda-Calculi
Ideas on this subject have been continuously evolving in the past one year, and they were collected so far in two technical reports. The newer technical report, listed first, contains our current view, therefore we recommend downloading this one.
Newer Technical Report
- Abstract. Generic first-order logic (GFOL) is a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring them to only provide generic notions of free variable and substitution satisfying reasonable properties. GFOL has a complete Gentzen system generalizing that of FOL. An important fragment of GFOL, called Horn^2, possesses a much simpler Gentzen system, similar to traditional context-based derivation systems of lambda-calculi. Horn^2 appears to be sufficient for defining virtually any lambda-calculi (including polymorphic and type-recursive ones) as theories inside the logic. GFOL endows its theories with a default loose semantics, complete for the specified calculi.
Older Technical Report
- Term-Generic First-Order Logic
- Andrei Popescu and Grigore Rosu
- Technical Report UIUCDCS-R-2006-2717, April 2006
- Abstract. Term-generic first-order logic, or simply generic first-order logic (GFOL), is presented as a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring them to only provide generic notions of free variable and substitution satisfying reasonable properties. A complete Gentzen deduction system is given, as well as complete equational and many-sorted extensions. It is shown that various calculi with binding, such as lambda-calculus and System F, can be faithfully defined as GFOL theories. Since GFOL is complete, by defining a logic or calculus as a GFOL theory one gets, at no additional effort, a semantics for that logic or calculus. A fragment of GFOL called Horn^2 is also defined, on whose theories, under certain conditions, the generic Gentzen deduction system is equivalent to a simplified deduction system which resembles the derivation system of the calculi that we intend to explicitly capture. Consequently, GFOL and especially its fragment Horn^2 can serve as a foundationaldefinitional framework for other calculi and logics, providing these with models and complete deduction.