Kudryavtsev V.B., Rosenberg I.G. Structural Theory of Automata, Semigroups, and Universal Algebra

Подождите немного. Документ загружается.

266 A. Letichevsky

conditional sequents. Now the transitions of a transition system are transitions of this calcu-

lus. Each transition corresponds to some inference rule. The states of successful termination

are axioms and a formula P is valid if aqnd only if one of the successful termination states is

reachable from the initial state (X

, 1, 1 ⇒ P ).

Let us label the transitions by actions. Each action is a message on which a rule has been

applied in the corresponding transition. For example a transition corresponding to the rule

of deleting a universal quantiﬁer is:

(X, s, w, u ⇒∀xp)

mes

−→ (addv(s, a),w,u ⇒ lsub(p, x := a))

where a message “To prove a statement ∀xp let us consider an arbitrary element a and prove

q” is used as an action mes where q =lsub(p, x := a). Other rules can be labeled in a

similar way. Proving a statement T is therefore reduced to ﬁnding the trace which labels the

transition of a system from the initial state (∅, ∅, 1, 1 ⇒ T ) to the state corresponding to one

of the axioms. If the axioms are deﬁned as the states of successful termination, the problem

is to ﬁnd the trace from the initial state to one of the successfully terminated states. The

sequence of messages corresponding to this trace is a text of a proof of a statement T .

This form of an evidence algorithm representation can be implemented in the system

of insertion programming using a trivial environment which allows arbitrary behavior of the

inserted agent. In automatic mode a system is looking for a trace with successful termination,

if possible, and prints the proof when the trace is found. In interactive mode a system

addresses to a user each time when it is necessary to make a non-deterministic choice. A

user is oﬀered several options to choose an inference rule and a user makes this choice. It

is possible to go back and jump to other brunches. An environment which provides such

possibilities is a proof system based on an evidence algorithm.

4.3 Decomposition of the transition system

A more interesting implementation of the evidence algorithm can be obtained if a state of

a calculus is split into an environment and an agent inserted into this environment. This

splitting is very natural if a substitution, partial order, conjunction of literals, or assumption

of a current sequent is considered as a state of the environment and the goal of the current

sequent, as well as all other sequents, is considered as an agent. Moreover it is possible to

change the conjunction of all other sequents to a sequential composition. Call this agent a

formula agent. A formula agent is considered as a state of the transition system used for the

representation of an agent. To compute the behavior of agents, a recursive unfolding function

must be deﬁned on the set of agent expressions. It is easy to extract the unfolding function

and the transition relation for a formula agent from the inference rules. Actions produced by

formula agent deﬁne necessary changes in the environment and are computed by the insertion

function. For example a formula agent (prove ∀xp; P ) is unfolded according to its recursive

deﬁnition to an agent expression Q = fresh C(∀xp).P ,wherefresh C(∀xp)isanaction

which substitutes a new ﬁxed variable for p. This substitution is performed by the insertion

function with transition

e[Q]

mes

−→ e



[prove lsub(p, x := a).P ],

where mes is a message considered before and the transition from e to e



corresponds to the

generation of a new ﬁxed a.

Algebra of behavior transformations 267

In a general extended conditional sequent

((X, s, w, u ⇒ v); P )

is decomposed into an environment state and a sequential composition of agents. The envi-

ronment state is

(X, s, w, u).

Initially (∅, ∅, 1, 1). The main types of agent expressions are:

• prove v; v is a simple sequent or formula,

• prove (H

∧ H

∧ ...); H

are simple sequents,

• block P ; P is an agent,

• end

block w; w is a conjunction of literals.

The following equations deﬁne unfolding and insertion function for blocks.

• prove (H

∧ H

∧ ...)=(prove H

; prove H

∧ ...);

• prove (u ⇒ v)=block (Let u.(ask 0.m

+ ask 1.m

.prove v).m

,where

– m

= mes (¬u is evident by contradiction);

– m

= mes (prove u ⇒ v);

– m

= mes (sequent proved);

• e[block P.Q]=mes(begin).e[P; end

block w; Q], where e =(X, s, w, F );

• e[end

block w



]=mes(end).e



[∆], where e



=(X, s, w



, 1) if e =(X, s,w, u).

Actions are easily recognized by dots following them. The meaning of actions mes x and

block P is clear from these deﬁnitions. Other actions will be explained later.

4.3.1 Unfolding conjunction and disjunction

In this section unfolding rules for conjunction and disjunction are explained as well as some

auxiliary rules.

prove (u ⇒ 0) = prove (¬u);

prove (x ∧ y)=(prove (x); prove (y));

prove (x ∨ y)=block(

Let (¬x).(

ask 0.mes (x is evident by contradiction)

ask 1.mes(To prove x ∨ y let ¬x, prove y).

prove (y)

); mes (disjunction proved)

)+(

Let ¬y.(

268 A. Letichevsky

ask 0.mes(y is evident by contradiction)

ask 1.mes(To prove x ∨ y let ¬y, prove x).

prove x

); mes(disjunction proved)

)

4.3.2 Unfolding quantiﬁers

In these deﬁnitions e



is a state of an environment after generating a new unknown (fresh V )

or ﬁxed (fresh C)variabley.

prove ∃xp =(fresh V prove ∃xp).∆;

prove ∀xp =(fresh C prove ∀xp).∆;

e[fresh Vq]=e



[get fresh yq];

e[fresh Cq]=e



[get fresh yq];

get

fresh y prove ∃xp = mes(

To prove ∃xp find x = y such that p

).block(

Let ¬∃xp.

prove lsub(p, x := y);

mes(existence proved)

);

get

fresh y prove ∀xp = mes(

Prove ∀xp. Let y is arbitrary constant.

).(

prove lsub(p, x := y);

mes(forall proved)

)

4.3.3 An auxiliary goal

The calculus of the auxiliary goal is implemented on the level of the environment. It is hidden

from an external observer who can only see the result, that is the auxiliary goal represented

by a corresponding message.

prove z = mes(To prove z find auxiliary goal).start

aux z;

e[start

aux z]=e



[prove aux(z, Q)];

prove

aux(z,1) = mes(z is evident);

prove

aux(z,Q)=mes(auxiliary goal is Q).prove Q.

Note that the rules for insertion of formula agents can be interpreted as one step insertions

except for the rules for start

aux and fresh. Both can be interpreted as an instantiation of

the rule:

−→ e



[v],u

−→ [u



]

e[u]

−→ e



[v; u



]

Algebra of behavior transformations 269

In the case of sequential insertion this rule can also be considered as a one-step insertion rule

because in this case e



[v; u



]=(e



[v])[u].

The last step in the development of an insertion program is veriﬁcation. The correctness

of the speciﬁcation calculi is proved as a sound and completeness theorem comparing it with

algorithms based on advanced tableau methods. After decomposition we should prove the

bisimilarity of the corresponding initial states of two systems. We can also improve the

insertion program. In this case we should do optimization preserving insertion equivalence

of agents.

4.4 A proving machine

Formula agent actions can be considered as instructions of a proving machine representing an

environment for such kind of agents. Here are some of the main instructions of the proving

machine used for the development of the evidence algorithm kernel.

• Let <formula> adds the formula to assumptions in the environment. It is used for

example for the unfolding sequent: prove (u ⇒ v)=Let u.prove v or for the unfolding

disjunction

prove (u ∨ v)=Let ¬v.prove v + Let ¬v.prove u.

An essential reconstruction of the environment is performed each time a new assumption

is added to the environment. Formulas are simpliﬁed, conjunctive literals are distin-

guished, substitution is applied etc. Moreover assumptions or a literal conjunction can

be simpliﬁed up to 0 (false).

• tell <literal> adds a literal to conjunction of literals without reconstruction of the

environment.

• ask 0 checks inconsistency of the environment state (0 in assumptions or in literals).

• ask 1 checks that there is no explicit inconsistency.

• start

aux <literal> starts the calculus of auxiliary goals:

e[start

aux p.Q]=Let ¬p.(prove P

+ prove P

+ ···)

where P

,... are auxiliary goals (conjunctions of sequents) extracted from assump-

tions according to the calculus of auxiliary goals (actually the real relations are slightly

more complex, because they include messages about the proof development and they

anticipate the case when there are no auxiliary goals at all).

• fresh V <formula> substitutes a new unknown into the formula.

• fresh C <formula> substitutes a new ﬁxed variable into the formula.

• solve <equation> is used for solving equations in the case when equality is used.

• block <program> localizes all assumptions within the block. It is used for example

when conjunction is proved.

• Mesg <text> inserts the printing of messages at the diﬀerent stages of the proof search.

270 A. Letichevsky

• start

lkb <literal>. It is used to address the local knowledge base for extracting

auxiliary goals from assumptions presented in this base. The local knowledge base is

prepared in advance according to requirements of the subject domain where the proof

is searched for.

The advantages of a proving machine (or more generally an insertion machine for other

environment structures) is that it is possible to change in a wide area the algorithms of a proof

search without changing the structure of the environment by varying the recursive unfolding

rules of formula agents. Moreover the environment itself can be extended by introducing new

instructions into the instruction set and adding new components to an environment state.

To run a program on a proving machine some higher level environment should be used

to implement back-tracking. Such an environment can work in two modes: interactive and

automatic. The following equations demonstrate the approximate meaning of these two

modes.

The interactive mode:

e[a

+ a

+ ...]=mes(select a

,...).(a



]+a



]+...)+back.e



[u]+∆.

The automatic mode:

e[a

+ a

+ ...]=e



[(a

); (return if fail or stop); (a

+ ...)].

This is a depth ﬁrst search. It works only with restrictions on the admissible depth. A

breadth ﬁrst search is more complex.

5 Conclusions

A model of interaction of agents and environments has been introduced and studied. The

ﬁrst two sections extend and generalize results previously obtained in [15]. The algebra of

behavior transformations is a good mathematical basis for the description and explanation

of agent behavior restricted by the environment in which it is inserted. System behavior has

two dimensions. The ﬁrst one is a branching time which deﬁnes the height of a behavior tree

and can be inﬁnite (but no more than countable). The second one is a non-deterministic

branching at a given point. Our construction of a complete behavior algebra used for the

characterization of bisimilarity allows for branching of arbitrary cardinality.

The restriction of the insertion function to be continuous is too broad and we consider

a more restricted classes of equationally deﬁned insertion functions and one-step insertions

to which more general head insertion is reduced. The question about reducing or restricting

look-ahead insertion is open at this moment. At the same time the algebra of behavior

transformations based on regular one-step insertion can be enriched by sequential and parallel

compositions.

The algebra of behavior transformations is the mathematical foundation of a new pro-

gramming paradigm: insertion programming. It has been successfully applied for automatic

theorem proving and veriﬁcation of distributed software systems. In [16] operational seman-

tics of timed MSC (speciﬁcation language of Message Sequencing Charts) has been deﬁned

on the basis of behavior transformations. This semantics has been used for the development

of tools for veriﬁcation of distributed systems.

Algebra of behavior transformations 271

References

[1] S. Abramsky, A domain equation for bisimulation, Information and Computation 92 (2)

(1991), 161–218.

[2] L. Aceto, W. Fokking, and C. Verhoef, Structural operational semantics, in: Handbook

of Process Algebra (J. A. Bergstra, A. Ponce, and S. A. Smolka, eds.), North-Holland,

2001.

[3] P. Aszel and N. Mendler, A ﬁnal coalgebra theorem, in: LNCS 389, Springer-Verlag,

1989.

[4] P. Azcel, J. Adamek, S. Milius, and J. Velebil, Inﬁnite trees and comletely iterative

theories: a coalgebraic view, TCS 300 (1–3) (2003), 1–45.

[5] J. A. Bergstra and J. W. Klop, Process algebra for synchronous communications, Infor-

mation and Control 60 (1/3) (1984), 109–137.

[6] J. A. Bergstra, A. Ponce, and S. A. Smolka, eds., Handbook of Process Algebra,North-

Holland, 2001.

[7] A. Degtyarev, J. Kapitonova, A. Letichevsky, A. Lyaletsky, and M. Morokhovets, Evi-

dence algorithm and problems of representation and processing of computer mathemat-

ical knowledge, Kibernetika and System Analysis (6) (1999), 9–17.

[8] R. J. Glabbeek, The linear time—branching time spectrum i. the semantics of concrete,

sequential processes, in: Handbook of Process Algebra (J. A. Bergstra, A. Ponce, and

S. A. Smolka, eds.), North-Holland, 2001.

[9] V. M. Glushkov, Automata theory and formal transformations of microprograms, Kiber-

netika (5).

[10] V. M. Glushkov and A. A. Letichevsky, Theory of algorithms and descrete processors,

in: Advances in Information Systems Science (J. T. Tou, ed.), vol. 1, Plenum Press,

1969.

[11] J. A. Goguen, S. W. Thetcher, E. G. Wagner, and J. B. Write, Initial algebra semantics

and continuous algebras, J. ACM (24) (1977), 68–95.

[12] M. Hennessy and R. Milner, On observing nondeterminism and concurrency, in: Proc.

ICALP’80, LNCS 85, Springer-Verlag, 1980.

[13] C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, 1985.

[14] A. Letichevsky, Algebras with approximation and recursive data structures, Kibernetika

and System Analysis (5) (1987), 32–37.

[15] A. Letichevsky and D. Gilbert, Interaction of agents and environments, in: Resent

trends in Algebraic Development technique, LNCS 1827 (D. Bert and C. Choppy, eds.),

Springer-Verlag, 1999.

272 A. Letichevsky

[16] A. Letichevsky, J. Kapitonova, V. Kotlyarov, A. Letichevsky, Jr., and V. Volkov, Se-

mantics of timed msc language, Kibernetika and System Analysis (4).

[17] A. Letichevsky, J. Kapitonova, V. Volkov, V. Vyshemirskii, and A. Letichevsky, Jr.,

Insertion programming, Kibernetika and System Analysis (1) (2003), 19–32.

[18] J. Meseguer, Conditional rewriting logic as a uniﬁed model of concurrency, Theoretical

Computer Science 96 (1992), 73–155.

[19] R. Milner, A Calculus of Communicating Systems,vol.92ofLecture Notes in Computer

Science, Springer-Verlag, 1980.

[20] R. Milner, Communication and Concurrency, Prentice Hall, 1989.

[21] R. Milner, The polyadic π-calculus: a tutorial, Tech. Rep. ECS–LFCS–91–180, Labora-

tory for Foundations of Computer Science, Department of Computer Science, University

of Edinburgh, UK (1991).

[22] D. Park, Concurrency and automata on inﬁnite sequences, in: LNCS 104, Springer-

Verlag, 1981.

[23] M. Roggenbach and M. Majster-Cederbaum, Towards a uniﬁed view of bisimulation: a

comparative study, TCS 238 (2000), 81–130.

[24] J. Rutten, Coalgebras and systems, TCS 249.

Congruence modular varieties: commutator theory

and its uses

Ralph MCKENZIE

Department of Mathematics

Vanderbilt University

Nashville, TN 37240

USA

John SNOW

Department of Mathematics

Concordia University

Seward, NE 68434

USA

Abstract

We present the basic theory of commutators of congruences in congruence modular

varieties (or equationally deﬁned classes) of algebras. The theory we present was ﬁrst

introduced to the mathematical world in a 1976 monograph of J. D. H. Smith, devoted to

varieties with permuting congruences. It was extended to congruence modular varieties

in a 1979 paper by J. Hagemann and C. Herrmann, and has since been elaborated into an

impressive machinery for attacking diverse problems in the domain of congruence modular

varieties. Three notable applications of this commutator theory are presented in detail,

and others are described.

1 Introduction

The commutator in group theory is a natural operation deﬁned on the lattice of normal

subgroups of any group which plays a basic role in the deﬁnition and study of solvable and

Abelian groups. This commutator has a companion operation in the theory of rings, deﬁned

on any lattice of ideals. These two operations share many common properties, including the

ability to capture the notion of Abelian-ness.

In [43], J. D. H. Smith used category theory to extend structural properties of groups

and rings to varieties with permuting congruences. In doing so, he laid the framework for

generalizing the commutator from groups and rings to an operation on the congruence lattices

of algebras in congruence permutable varieties.

J. Hagemann and C. Herrmann in [19] extended some of Smith’s results to congru-

ence modular varieties. Their techniques include subtle and diﬃcult calculations in Con A,

Con A

,andConA

using modular arithmetic. In their work, they mentioned the term

273

V. B. Kudryavtsev and I. G. Rosenberg (eds.),

Structural Theory of Automata, Semigroups, and Universal Algebra, 273–329.

274 R. McKenzie and J. Snow

condition which would later become the basis for what seems to be the most useful deﬁni-

tion of the commutator in congruence modular varieties. H.-P. Gumm [17] further extended

these structural results for congruence modular varieties by viewing the structure imposed

on algebras by congruence relations geometrically. R. Freese and R. McKenzie [12] developed

the commutator for congruence modular varieties based on the term condition mentioned by

Hagemann and Herrmann.

In this manuscript, we give a gentle introduction to the commutator theory presented in

[12]. We then present several applications of the commutator along with some open problems

which may involve commutator theory. In Section 2 we review the classical commutator in

groups and demonstrate how the term condition arises naturally in this environment. In

Section 3 we lay out some basic notation which will be pervasive throughout the manuscript.

In Section 4 we use the notion of centrality to deﬁne the commutator and prove a few

properties of the commutator which hold in any environment. In Section 5 we give examples

of the commutator in some familiar environments including rings, lattices, and modules. In

Section 6 we give the classical Maltsev type characterizations of congruence permutability,

distributivity, and modularity due to Maltsev, J´onsson, and Day. These characterizations are

exploited heavily in the development of commutator theory for congruence modular varieties.

In Section 7 we use J´onsson’s characterization of congruence distributivity to prove that in a

congruence distributive variety the commutator is nothing other than congruence intersection.

In Section 8 we extend all of the properties of the group commutator mentioned in Section 2

to the commutator in congruence modular varieties. In Section 9 we prove the Fundamental

Theorem of Abelian Algebras that every Abelian algebra (in a congruence modular variety) is

aﬃne (polynomially equivalent to a module). In Section 10 we extend the ideas of solvability

and nilpotence using the commutator. We prove that every nilpotent or solvable algebra

in a congruence modular variety has a Maltsev term and use this to give some structural

results about nilpotent algebras. In Section 11 on applications, we brieﬂy discuss seven

outstanding instances of basic problems that have been solved, for modular varieties, with

the aid of commutator theory. In the following sections, we present three of these applications

in detail: In Section 12 we prove that every ﬁnitely generated, residually small, congruence

modular variety has a ﬁnite residual bound, and that such varieties are characterized by a

commutator equation. In Section 13 we characterize directly representable varieties—i.e.,

those ﬁnitely generated varieties that possess only a ﬁnite number of non-isomorphic ﬁnite,

directly indecomposable, algebras—and we characterize the larger family of ﬁnitely generated

varieties whose spectrum is contained in a ﬁnitely generated monoid of positive integers. All

of these varieties are shown to be congruence modular. In Section 14 we characterize the

locally ﬁnite congruence modular varieties for which the function giving the number of non-

isomorphic n-generated algebras is dominated by a polynomial in n. They are precisely the

directly representable Abelian varieties. In Section 15 we survey some problems which either

involve the commutator or for which there is evidence that the commutator might prove

useful. We note that the results herein are not original. Excepting the results of Sections 13–

14, almost all of them appear with proofs in [12].

2 The commutator in groups

In this section, we discuss the group commutator and some of its most basic properties, and

we illustrate how the term condition arises naturally in this environment.

Congruence modular varieties 275

2.1 Deﬁnition Suppose that G is a group and M and N are normal subgroups of G.The

group commutator of M and N is deﬁned as

[M,N]=Sg

({m

−1

mn : m ∈ M and n ∈ N}), (2.1)

Suppose that G is a group, that M, N,and{N

: i ∈ I} are normal subgroups of G,and

that f : G → H is a surjective group homomorphism. Then the following properties of the

group commutator are easy exercises in any ﬁrst class on group theory.

(1) [M,N] ⊆ M ∩ N .

(2) f([M,N]) = [f (M),f(N)].

(3) [M,N]=[N, M].

(4) [M,



i∈I



i∈I

[M,N

(5) For any normal subgroup K of G included in M ∩N, the elements of M/K commute

with the elements of N/K if and only if K ⊇ [M, N].

(6) G is Abelian if and only if [G, G]={1} (where 1 is the identity element of G).

When we generalize the commutator later to congruences in a congruence modular variety,

we will want an operation which will share these properties. Our operation will be deﬁned

from a generalization of the condition (5). From this deﬁnition, we will get (1), (3), and (4)

directly and a slight modiﬁcation of (2). We will take (6) to be our deﬁnition of Abelian.

The group commutator has one more property which is less transparent but which will

also carry over to the generalization (in fact, it also could be used to deﬁne the modular

commutator). This is

(7) The commutator operation is the largest binary operation deﬁned across all normal

subgroup lattices of all groups which satisﬁes conditions (1) and (5).

Suppose that C(x, y) is another binary operation deﬁned on the normal subgroup lattice

of every group which satisﬁes (1) and (2). Let M and N be normal subgroups of a group G.

We will prove that C(M,N) ⊆ [M, N]. To do so, we need to deﬁne four subgroups of G ×G.

G(M)={x, y : x, y ∈ G and x

−1

y ∈ M} (2.2)

∆={x, y : x ∈ N,y ∈ G, and x

−1

y ∈ [M, N]} (2.3)

B = {x, 1 : x ∈ [M,N]} (2.4)

= {x, 1 : x ∈ M }. (2.5)

The subgroups ∆, B,andM

are normal subgroups of G(M ). Let π be the projection of

G(M) onto the ﬁrst coordinate. Then the reader can check that

π(G(M)) = G (2.6)

π(∆) = N (2.7)

π(B)=[M,N] (2.8)

π(M

)=M. (2.9)