An algebraic theory of clones Bucciarelli, Antonio; Salibra, Antonino
Algebra universalis,
05/2022, Letnik:
83, Številka:
2
Journal Article
Recenzirano
We introduce the notion of
clone algebra
(
CA
), intended to found a one-sorted, purely algebraic theory of clones.
CA
s are defined by identities and thus form a variety in the sense of universal ...algebra. The most natural
CA
s, the ones the axioms are intended to characterise, are algebras of functions, called
functional clone algebras
(
FCA
). The universe of a
FCA
, called
ω
-
clone
, is a set of infinitary operations on a given set, containing the projections and closed under finitary compositions. The main result of this paper is the general representation theorem, where it is shown that every
CA
is isomorphic to a
FCA
and that the variety
CA
is generated by the class of finite-dimensional
CA
s. This implies that every
ω
-clone is algebraically generated by a suitable family of clones by using direct products, subalgebras and homomorphic images. We conclude the paper with two applications. In the first one, we use clone algebras to give an answer to a classical question about the lattices of equational theories. The second application is to the study of the category of all varieties of algebras.
Ordered Models of the Lambda Calculus Salibra, Antonino; Carraro, Alberto
Logical methods in computer science,
12/2013, Letnik:
9, Issue 4
Journal Article
Recenzirano
Odprti dostop
Answering a question by Honsell and Plotkin, we show that there are two
equations between lambda terms, the so-called subtractive equations, consistent
with lambda calculus but not simultaneously ...satisfied in any partially ordered
model with bottom element. We also relate the subtractive equations to the open
problem of the order-incompleteness of lambda calculus, by studying the
connection between the notion of absolute unorderability in a specific point
and a weaker notion of subtractivity (namely n-subtractivity) for partially
ordered algebras. Finally we study the relation between n-subtractivity and
relativized separation conditions in topological algebras, obtaining an
incompleteness theorem for a general topological semantics of lambda calculus.
The stack calculus Carraro, Alberto; Ehrhard, Thomas; Salibra, Antonino
Electronic proceedings in theoretical computer science,
3/2013, Letnik:
113, Številka:
Proc. LSFA 2012
Journal Article
Odprti dostop
We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry-Howard correspondence for Classical Logic can be faithfully ...encoded. Our calculus enjoys confluence without any restriction. Its type system enforces strong normalization of expressions and it is a sound and complete system for full implicational Classical Logic. We give a very simple denotational semantics which allows easy calculations of the interpretation of expressions.
The universal algebraic literature is rife with generalisations of discriminator varieties, whereby several investigators have tried to preserve in more general settings as much as possible of their ...structure theory. Here, we modify the definition of discriminator algebra by having the switching function project onto its third coordinate in case the ordered pair of its first two coordinates belongs to a designated relation (not necessarily the diagonal relation). We call these algebras factor algebras and the varieties they generate factor varieties. Among other things, we provide an equational description of these varieties and match equational conditions involving the factor term with properties of the associated factor relation. Factor varieties include, apart from discriminator varieties, several varieties of algebras from quantum and fuzzy logics.
We establish a connection between skew Boolean algebras and Church algebras. We prove that the set of all semicentral elements in a right Church algebra forms a right-handed skew Boolean algebra for ...the properly defined operations. The main result of this paper states that the variety of all semicentral right Church algebras of type
τ
is term equivalent to the variety of right-handed skew Boolean algebras with additional regular operations. As a corollary to this result, we show that a pointed variety is a discriminator variety if and only if it is a 0-regular variety of right-handed skew Boolean algebras.
We develop a new general framework for algebras and clones, called Universal Clone Algebra. Algebras and clones of finitary operations are to Universal Algebra what t-algebras and clone algebras are ...to Universal Clone Algebra. Clone algebras have been recently introduced to found a one-sorted, purely algebraic theory of clones, while t-algebras are first introduced in this article. We present a method to codify algebras and clones into t-algebras and clone algebras, respectively. We provide concrete examples showing that general results in Universal Clone Algebra, when translated in terms of algebras and clones, give more powerful versions of known theorems in Universal Algebra. We apply this methodology to Birkhoff's HSP theorem and to the recent topological versions of Birkhoff's theorem.
Easy lambda-terms are not always simple Carraro, Alberto; Salibra, Antonino
RAIRO. Informatique théorique et applications,
04/2012, Letnik:
46, Številka:
2
Journal Article
Recenzirano
Odprti dostop
A closed λ-term M is easy if, for any other closed term N, the lambda theory generated by M = N is consistent. Recently, it has been introduced a general technique to prove the easiness of λ-terms ...through the semantical notion of simple easiness. Simple easiness implies easiness and allows to prove consistency results via construction of suitable filter models of λ-calculus living in the category of complete partial orderings: given a simple easy term M and an arbitrary closed term N, it is possible to build (in a canonical way) a non-trivial filter model which equates the interpretation of M and N. The question whether easiness implies simple easiness constitutes Problem 19 in the TLCA list of open problems. In this paper we negatively answer the question providing a non-empty co-r.e. (complement of a recursively enumerable) set of easy, but not simple easy, λ-terms.
Using Vaggione’s concept of central element in a double-pointed algebra, we introduce the notion of
Boolean-like variety
as a generalisation of Boolean algebras to an arbitrary similarity type. ...Appropriately relaxing the requirement that every element be central in any member of the variety, we obtain the more general class of
semi-Boolean-like varieties
, which still retain many of the pleasing properties of Boolean algebras. We prove that a double-pointed variety is discriminator if and only if it is semi-Boolean-like, idempotent, and 0-regular. This theorem yields a new Maltsev-style characterisation of double-pointed discriminator varieties.
Clones of operations of arity \(\omega\) (referred to as \(\omega\)-operations) have been employed by Neumann to represent varieties of infinitary algebras defined by operations of at most arity ...\(\omega\). More recently, clone algebras have been introduced to study clones of functions, including \(\omega\)-operations, within the framework of one-sorted universal algebra. Additionally, polymorphisms of arity \(\omega\), which are \(\omega\)-operations preserving the relations of a given first-order structure, have recently been used to establish model theory results with applications in the field of complexity of CSP problems. In this paper, we undertake a topological and algebraic study of polymorphisms of arity \(\omega\) and their corresponding invariant relations. Given a Boolean ideal \(X\) on the set \(A^\omega\), we propose a method to endow the set of \(\omega\)-operations on \(A\) with a topology, which we refer to as \(X\)-topology. Notably, the topology of pointwise convergence can be retrieved as a special case of this approach. Polymorphisms and invariant relations are then defined parametrically, with respect to the \(X\)-topology. We characterise the \(X\)-closed clones of \(\omega\)-operations in terms of \(Pol^\omega\)-\(Inv^\omega\) and present a method to relate \(Inv^\omega\)-\(Pol^\omega\) to the classical (finitary) \(Inv\)-\(Pol\).
Factor Varieties and Symbolic Computation Salibra, Antonino; Manzonetto, Giulio; Favro, Giordano
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science,
07/2016
Conference Proceeding
Odprti dostop
We propose an algebraization of classical and non-classical logics, based on factor varieties and decomposition operators. In particular, we provide a new method for determining whether a ...propositional formula is a tautology or a contradiction. This method can be automatized by defining a term rewriting system that enjoys confluence and strong normalization. This also suggests an original notion of logical gate and circuit, where propositional variables becomes logical gates and logical operations are implemented by substitution. Concerning formulas with quantifiers, we present a simple algorithm based on factor varieties for reducing first-order classical logic to equational logic. We achieve a completeness result for first-order classical logic without requiring any additional structure.
PDF
