Complexity of Commutative Infinitary Action Logic
We consider commutative infinitary action logic, that is, the equational theory of commutative *-continuous action lattices, and show that its derivability problem is \(\varPi _1^0\) -complete. Thus, we obtain a commutative version of \(\varPi _1^0\) -com
- PDF / 314,504 Bytes
- 15 Pages / 439.37 x 666.142 pts Page_size
- 56 Downloads / 184 Views
Abstract. We consider commutative infinitary action logic, that is, the equational theory of commutative *-continuous action lattices, and show that its derivability problem is Π10 -complete. Thus, we obtain a commutative version of Π10 -completeness for non-commutative infinitary action logic by Buszkowski and Palka (2007). The proof of the upper bound is more or less the same as Palka’s argument. For the lower bound, we encode non-terminating behaviour of two-counter Minsky machines. Keywords: Complexity lattices
1
· Infinitary action logic · Commutative action
Introduction
Action logic is the equational theory (algebraic logic) for action lattices, that is, Kleene lattices with residuals. The concept of action lattice, introduced by Pratt [17] and Kozen [8], combines several algebraic structures: a partially ordered monoid with residuals (“multiplicative structure”), a lattice (“additive structure”) sharing the same partial order, and Kleene star. (Pratt introduced the notion of action algebra, which bears only a semi-lattice structure with join, but not meet. Action lattices are due to Kozen.)
is a partial order on A; 0 is the smallest element for , that is, 0 a for any a ∈ A; A; ·, 1 is a monoid; and are residuals of the product (·) w.r.t. , that is:
b a c ⇐⇒ a · b c ⇐⇒ a c
1. 2. 3. 4.
, ∨, ∧, ∗ ,
Definition 1. An action lattice is a structure A; , ·, 0, 1, , where:
b;
5. A; , ∨, ∧ is a lattice; 6. for each a ∈ A, a∗ = min {b | 1 b and a · b b}. An important subclass of action lattices is formed by *-continuous action lattices. c Springer Nature Switzerland AG 2020 M. A. Martins and I. Sedl´ ar (Eds.): DaL´ı 2020, LNCS 12569, pp. 155–169, 2020. https://doi.org/10.1007/978-3-030-65840-3_10
156
S. Kuznetsov
Definition 2. Action lattice A is *-continuous, if for any a ∈ A we have a∗ = sup {an | n ≥ 0}, where an = a · . . . · a (n times) and a0 = 1. Interesting examples of action lattices are mostly *-continuous; non-*-continuous action lattices also exist, but are constructed artificially. The equational theory for the class of action lattices or its subclass (e.g., the class of *-continuous action lattices) is the set of all statements of the form A B, where A and B are formulae (terms) built from variables and constants 0 and 1 using action lattice operations, which are true in any action lattice from the given class under any valuation of variables. More precisely, the previous sentence defines the inequational theory, but in the presence of lattice operations it is equivalent to the equational one: A B can be equivalently represented as A ∨ B = B. In a different terminology, equational theories of classes of action lattices are seen as algebraic logics. These logics are substructural, extending the multiplicative-additive (“full”) Lambek calculus [6,13], which is a non-commutative intuitionstic variant of Girard’s linear logic [4]. The equational theory of all action lattices is called action logic and denoted by ACT. For the subclass of *-continuous ac
Data Loading...
