The functional lambda abstraction algebras form a variety

The algebraic counterparts of the usual semantics for the untyped \(\lambda\)-calculus are the \(\lambda\)-abstraction algebras, introduced by \textit{D. Pigozzi} and \textit{A. Salibra} in Theor. Comput. Sci. 140, No. 1, 5-52 (1999; Zbl 0874.68188). Just like algebras of sets are the ``concrete Boolean algebras, concrete examples of \(\lambda\)-abstraction algebras are the functional algebras (FLA) and relativized functional algebras (RFA) considered in this paper. A domain \(V\) is a structure \((V,\cdot,\lambda)\) where \(\cdot\) is a binary operation (application) and \(\lambda\) is a map (abstraction) from a subset of \(V^V\) into \(V\) such that \(\lambda(f) \dots v=f(v)\). An environment is a member of \(V^I\). Very roughly speaking, an FLA on the domain \(V\) is a subalgebra of the power \(V^{V^1}\) while an RFA is a subalgebra of some power \(V^{V^I_r}\), where \(V^I_r\) is the set of environments which agree with \(r\) \((\in V^I)\) on a cofinite subset of \(I\). It is known that the class IRFA of isomorphic copies of RFA is a variety. Here the authors show that any RFA \(A\) is isomorphic to an FLA on a domain that is an ultrapower of the domain of \(A\). This shows in particular that IFLA is a variety (the same as IRFA), solving positively an open problem. For the entire collection see [Zbl 0892.00029].

Recommendations

Cited in

(5)

This page was built for publication: The functional lambda abstraction algebras form a variety

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4217595)