|
|
|---|
|
|
|
|---|
A formalization of ACL2 translated terms.
ACL2 terms may be untranslated (i.e. user-facing) or translated (i.e. internal). Here we formalize translated terms, which we essentially regard as abstract syntax of the ACL2 programming language. We may also formalize untranslated terms at some point, but for now it seems that translated terms should suffice for an initial formalization of the ACL2 programming language.
We formalize translated terms as free algebraic structures, without the world-related constraints (e.g. that all function symbols are in the world), and even without some of the constraints included in pseudo-termp (e.g. that the number of actual arguments of a lambda call matches the number of parameters of the lambda expression). These well-formedness constraints may be formalized separately.
We use (free) fixtypes to formalize translated terms. As noted above, these fixtypes are a bit larger than pseudo-termp. Thus, the fixtypes introduced here differ slightly from the pseudo-term fixtypes, which are consistent with pseudo-termp and also include an explicit notion of `null' term.