Axiomatization of if-then-else over monoids of possibly non-halting programs and tests
Gayatri Panicker
Department of Mathematics, Indian Institute of Technology Guwahati, Guwahati, India
[email protected]
,
K. V. Krishna
Department of Mathematics, Indian Institute of Technology Guwahati, Guwahati, India
[email protected]
and
Purandar
Bhaduri
Department of Computer Science and Engineering, Indian Institute of Technology Guwahati, Guwahati, India
[email protected]
Abstract.
In order to study the axiomatization of the if-then-else construct over possibly non-halting programs and tests, the notion of C-sets was introduced in the literature by considering the tests from an abstract C-algebra. This paper extends the notion of C-sets to C-monoids which include the composition of programs as well as composition of programs with tests. For the class of C-monoids where the C-algebras are adas a canonical representation in terms of functional C-monoids is obtained.
Key words and phrases:
Axiomatization, if-then-else, non-halting programs, C-algebra
2010 Mathematics Subject Classification:
08A70, 03G25 and 68N15.
Introduction
The algebraic properties of the program construct if-then-else have been studied in great detail under various contexts. For example, in [8, 17, 21], the authors investigated on axiom schema for determination of the semantic equivalence between the conditional expressions. The authors in [2, 5, 18] studied complete proof systems for various versions of if-then-else. While a transformational characterization of if-then-else was given in [16], an axiomatization of equality test algebras was considered in [9, 20]. In [1, 22], if-then-else was studied as an action of Boolean algebra on a set. Due to their close relation with program features, functions have been canonical models for studies on algebraic semantics of programs.
In [12] Kennison defined comparison algebras as those equipped with a quaternary operation C(s,t,u,v) satisfying certain identities modelling the equality test. He also showed that such algebras are simple if and only if C is the direct comparison operation C0 given by C0(s,t,u,v) taking value u if s=t and v otherwise. This was extended by Stokes in [23] to semigroups and monoids. He showed that every comparison semigroup (monoid) is embeddable in the comparison semigroup (monoid) T(X) of all total functions X→X, for some set X. He also obtained a similar result in terms of partial functions X→X. In [10] Jackson and Stokes gave a complete axiomatization of if-then-else over halting programs and tests. They also modelled composition of functions and of functions with predicates and called this object a B-monoid and further showed that the more natural setting of only considering composition of functions would not admit a finite axiomatization. They proved that every B-monoid is embeddable in a functional B-monoid comprising total functions and halting tests and thus achieved a Cayley-type theorem for the class of B-monoids.
The work listed above predominantly considered the case where the tests are halting and drawn from a Boolean algebra. A natural interest is to study non-halting tests and programs.
There are multiple studies (e.g., see [3, 7, 13, 14]) on extending two-valued Boolean logic to three-valued logic. However McCarthy’s logic (cf. [17]) is distinct in that it models the short-circuit evaluation exhibited by programming languages that evaluate expressions in sequential order, from left to right. In [6] Guzmán and Squier gave a complete axiomatization of McCarthy’s three-valued logic and called the corresponding algebra a C-algebra, or the algebra of conditional logic. While studying if-then-else algebras in [15], Manes defined an ada (Algebra of Disjoint Alternatives) which is essentially a C-algebra equipped with an oracle for the halting problem.
Jackson and Stokes in [11] studied the algebraic theory of computable functions, which can be viewed as possibly non-halting programs, together with composition, if-then-else and while-do. In this work they assumed that the tests form a Boolean algebra. Further, they demonstrated how an algebra of non-halting tests could be constructed from Boolean tests in their setting. Jackson and Stokes proposed an alternative approach by considering an abstract collection of non-halting tests and posed the following problem:
Characterize the algebras of computable functions associated with an abstract C-algebra of non-halting tests.
The authors in [19] have approached the problem by adopting the approach of Jackson and Stokes in [10]. The notion of a C-set was introduced through which a complete axiomatization for if-then-else over a class of possibly non-halting programs and tests, where tests are drawn from an ada, was provided.
In this paper, following the approach of Jackson and Stokes in [10], we extend the notion of C-sets to include composition of possibly non-halting programs and of these programs with possibly non-halting tests. This object is termed a C-monoid and we show that every C-monoid where the tests are drawn from an ada is embeddable in a canonical model of C-monoids, viz., functional C-monoids. The organisation of the paper is as follows. In Section 1 we provide necessary background material including the notion of C-sets and their properties. We introduce the notion of a C-monoid in Section 2 and give various examples thereof. In Section 3 we delineate the procedure to achieve a Cayley-type theorem and embed every C-monoid where the tests are drawn from an ada into a functional C-monoid. We conclude the paper in Section 4.
1. Preliminaries
In this section we present the necessary background material. First we recall the concept of B-sets. The notion of a B-set was introduced by Bergman in [1] and elucidated by Jackson and Stokes in [10] to study the theory of halting programs equipped with the operation of if-then-else.
Definition 1.1**.**
Let ⟨Q,∨,∧,¬,T,F⟩ be a Boolean algebra and S
be a set. A B-set is a pair (S,Q), equipped with a function η:Q×S×S→S, called B-action, where η(α,a,b) is denoted by α[a,b], read “if α then a else b”, that satisfies the following axioms for all α,β∈Q and a,b,c∈S:
[TABLE]
In [10] Jackson and Stokes also considered the case of modelling if-then-else over a collection of programs with composition by including an operation to capture the composition of programs with tests.
Definition 1.2**.**
Let (S,⋅) be a monoid with identity element 1 and (S,Q) be a B-set. The pair (S,Q) equipped with a function ∘:S×Q→Q is said to be a B-monoid if it satisfies the following axioms for all a,b,c∈S and α,β∈Q:
[TABLE]
Since functions on sets model programs, standard examples of B-sets and B-monoids come from functions on sets. Let X and Y be two sets. The set of all functions X→Y will be denoted by YX while the set of all functions X→X will be denoted by T(X).
Let 2 be the two element Boolean algebra. For any set X the pair (T(X),2X) is a B-set with the following action for all α∈2X and g,h∈T(X):
[TABLE]
Note that T(X) is a monoid with respect to usual composition of mappings. The B-set (T(X),2X) equipped with the operation ∘ defined by
[TABLE]
for all f∈T(X) and α∈2X is a B-monoid. In fact, Jackson and Stokes obtained the following theorem.
Theorem 1.3** ([10]).**
Every B-monoid (S,Q) is embeddable as a two-sorted algebra into the B-monoid (T(X),2X) for some set X. Furthermore, if S and Q are finite, then X is finite.
In [6] Guzmán and Squier introduced the notion of a C-algebra as the algebra corresponding to McCarthy’s three-valued logic (cf. [17]).
Definition 1.4**.**
A C-algebra is an algebra ⟨M,∨,∧,¬⟩ of
type (2,2,1), which satisfies the following axioms for all α,β,γ∈M:
[TABLE]
It is easy to see that every Boolean algebra is a C-algebra. In particular, 2 is a C-algebra. Let 3 denote the C-algebra with the universe {T,F,U} and the following operations.
[TABLE]
[TABLE]
[TABLE]
In fact, the C-algebra 3 is the McCarthy’s three-valued logic.
In view of the fact that the class of C-algebras is a variety, for any set X, 3X is a C-algebra with the operations defined pointwise. Guzmán and Squier in [6] showed that elements of 3X along with the C-algebra operations may be viewed in terms of pairs of sets. This is a pair (A,B) where A,B⊆X and A∩B=∅. Akin to the well-known correlation between 2X and the power set \raisebox{1.79993pt}{\Large\wp}(X) of X, for any element α∈3X, associate the pair of sets (α−1(T),α−1(F)). Conversely, for any pair of sets (A,B) where A,B⊆X and A∩B=∅ associate the function α where α(x)=T if x∈A, α(x)=F if x∈B and α(x)=U otherwise. With this correlation, the operations can be expressed as follows:
[TABLE]
Notation 1.5**.**
We use M to denote an arbitrary C-algebra. By a C-algebra with T,F,U we mean a C-algebra with nullary operations T,F,U, where T is the (unique) left-identity (and right-identity) for ∧, F is the (unique) left-identity (and right-identity) for ∨ and U is the (unique) fixed point for ¬. Note that U is also a left-zero for both ∧ and ∨ while F is a left-zero for ∧.
In [15] Manes introduced the notion of ada (algebra of disjoint alternatives) which is a C-algebra equipped with an oracle for the halting problem.
Definition 1.6**.**
An ada is a C-algebra M with T,F,U equipped with an additional unary operation ( )↓ subject to the following equations for all α,β∈M:
[TABLE]
The C-algebra 3 with the unary operation ( )↓ defined by (22), (23) and (24) forms an ada. This ada will also be denoted by 3. One may easily resolve the notation overloading – whether 3 is a C-algebra or an ada – depending on the context. In [15] Manes showed that the ada 3 is the only subdirectly irreducible ada. For any set X, 3X is an ada with operations defined pointwise. Note that the ada 3 is also simple.
We use the following notations related to sets and equivalence relations.
Notation 1.7**.**
- (1)
Let X be a set and ⊥∈/X. The pointed set X∪{⊥} with base point ⊥ is denoted by X⊥.
2. (2)
The set of all functions on X⊥ which fix ⊥ is denoted by To(X⊥), i.e., To(X⊥)={f∈T(X⊥):f(⊥)=⊥}.
3. (3)
Under an equivalence relation σ on a set A, the equivalence class of an element p∈A will be denoted by pσ. Within a given context, if there is no ambiguity, we may simply denote the equivalence class by p.
In order to axiomatize if-then-else over possibly non-halting programmes and tests, in [19], Panicker et al. considered the tests from a C-algebra and introduced the notion of C-sets. We now recall the notion of a C-set.
Definition 1.8**.**
Let S⊥ be a pointed set with base point ⊥ and M be a C-algebra with T,F,U. The pair (S⊥,M) equipped with an action
[TABLE]
is called a C-set if it satisfies the following axioms for all α,β∈M and s,t,u,v∈S⊥:
[TABLE]
Let M be a C-algebra with T,F,U treated as a pointed set with base point U. The pair (M,M) is a C-set under the following action for all α,β,γ∈M:
[TABLE]
We denote the action of the C-set (M,M) by _[[_,_]]. In [19], Panicker et al. showed that the axiomatization is complete for the class of C-sets (S⊥,M) when M is an ada. In that connection, they obtained some properties of C-sets. Amongst, in Proposition 1.9 below, we list certain properties related to congruences which are useful in the present work. Viewing C-sets as two-sorted algebras, a congruence of a C-set is a pair (σ,τ), where σ is an equivalence relation on S⊥ and τ is a congruence on the ada M such that (s,t),(u,v)∈σ and (α,β)∈τ imply that (α[s,u],β[t,v])∈σ.
Proposition 1.9** ([19]).**
Let (S⊥,M) be a C-set where M is an ada. For each maximal congruence θ on M, let Eθ be the relation on S⊥ given by
[TABLE]
Then we have the following properties:
- (i)
For α∈M and s,t∈S⊥, if (α,β)∈θ then according to β=T,F or U, we have (α[s,t],s)∈Eθ,(α[s,t],t)∈Eθ or (α[s,t],⊥)∈Eθ, respectively.
2. (ii)
The pair (Eθ,θ) is a C-set congruence.
3. (iii)
For the C-set (M,M) the equivalence Eθ on M, denoted by EθM, is a subset of θ.
4. (iv)
θ⋂Eθ=ΔS⊥, where θ ranges over all maximal congruences on M.
5. (v)
The intersection of all maximal congruences on M is trivial, that is ⋂θ=ΔM where θ ranges over all maximal congruences on M.
For more details on C-sets one may refer to [19].
2. C-monoids
We now include the case where the composition of two elements of the base set and of an element with a predicate is allowed. Our motivating example is (To(X⊥),3X), where To(X⊥) is considered to be a monoid with zero by equipping it with composition of functions. The composition will be written from left to right, i.e., (f⋅g)(x)=g(f(x)). The monoid identity in To(X⊥) is the identity function idX⊥ and the zero element is ζ⊥, the constant function taking the value ⊥. We also include composition of functions with predicates via the natural interpretation given by the following for all f∈To(X⊥) and α∈3X:
[TABLE]
Note that if the composition takes value T or F at some point x∈X⊥ then as α∈3X this implies that f(x)=⊥.
With this example in mind we define a C-monoid as follows.
Definition 2.1**.**
Let (S⊥,⋅) be a monoid with identity element 1 and zero element ⊥ where ⊥⋅s=⊥=s⋅⊥. Let M be a C-algebra and (S⊥,M) be a C-set with ⊥ as the base point of the pointed set S⊥. The pair (S⊥,M) equipped with a function
[TABLE]
is said to be a C-monoid if it satisfies the following axioms for all s,t,r,u∈S⊥ and α,β∈M:
[TABLE]
The following are examples of C-monoids.
Example 2.2**.**
Recall from [19] that the pair \big{(}\mathcal{T}_{o}(X_{\bot}),\mathbb{3}^{X}\big{)} equipped with the action (46) for all f,g∈To(X⊥) and α∈3X is a C-set. Note that To(X⊥) is treated as a pointed set with base point ζ⊥.
[TABLE]
The C-set \big{(}\mathcal{T}_{o}(X_{\bot}),\mathbb{3}^{X}\big{)} equipped with the operation ∘ given in (36) and with To(X⊥) treated as a monoid with zero is in fact a C-monoid. For verification of axioms (37) – (45) refer to Appendix A.1. Such C-monoids will be called functional C-monoids.
Example 2.3**.**
Let S⊥ be a non-trivial monoid with identity 1 and zero ⊥ and no non-zero zero-divisors, i.e., s⋅t=⊥⇒s=⊥ or t=⊥. Then S⊥X is also a monoid with zero for any set X with operations defined pointwise. For f,g∈S⊥X define (f⋅g)(x)=f(x)⋅g(x). The identity of S⊥X is the constant function ζ1 taking the value 1. The zero and base point of S⊥X is the constant function ζ⊥ taking the value ⊥. Recall from [19] that the pair \big{(}S_{\bot}^{X},\mathbb{3}^{X}\big{)} is a C-set under action (46). In fact it is also a C-monoid with ∘ defined as follows for all f∈S⊥X and α∈3X:
[TABLE]
For verification of axioms (37) – (45) refer to Appendix A.2.
Example 2.4**.**
Let S⊥ be a non-trivial monoid with zero and no non-zero zero-divisors, i.e., s⋅t=⊥⇒s=⊥ or t=⊥. In [19] the authors showed that for any pointed set S⊥ with base point ⊥, the pair (S⊥,3) is a (basic) C-set with respect to the following action for all a,b∈S⊥ and α∈3:
[TABLE]
This basic C-set (S⊥,3) equipped with ∘:S⊥×3→3 defined below for all s∈S⊥ and α∈3 is a C-monoid.
[TABLE]
For verification of axioms (37) – (45) refer to Appendix A.3.
3. Representation of a class of C-monoids
In this section we obtain a Cayley-type theorem for a class of C-monoids as stated in the following main theorem.
Theorem 3.1**.**
Every C-monoid (S⊥,M) where M is an ada is embeddable in the C-monoid \big{(}\mathcal{T}_{o}(X_{\bot}),\mathbb{3}^{X}\big{)} for some set X. Moreover, if both S⊥ and M are finite then so is X.
Sketch of the proof. For each maximal congruence θ of M, we consider the C-set congruence (Eθ,θ) of (S⊥,M). Corresponding to each such congruence, we construct a homomorphism of C-monoids from (S⊥,M) to the functional C-monoid over the set S⊥/Eθ. This collection of homomorphisms has the property that every distinct pair of elements from each component of the C-monoid will be separated by some homomorphism from this collection. We then set X to be the disjoint union of S⊥/Eθ’s excluding the equivalence class ⊥Eθ. We complete the proof by constructing a monomorphism – by pasting together each of the individual homomorphisms from the collection defined earlier – from the C-monoid (S⊥,M) to the functional C-monoid over the pointed set X⊥ with a new base point ⊥.
The proof of Theorem 3.1 will be developed through various subsections. First in Subsection 3.1, we study some properties of maximal congruences of adas. We then present a collection of homomorphisms which separate every distinct pair of elements from each component of (S⊥,M) in Subsection 3.2. In Subsection 3.3, we construct the required functional C-monoid and establish an embedding from (S⊥,M). Finally, we consolidate the proof in Subsection 3.4.
In what follows (S⊥,M) is a C-monoid with M as an ada. Let θ be a maximal congruence on M and Eθ be the equivalence on S⊥ as defined in Proposition 1.9 so that the pair (Eθ,θ) is a congruence on (S⊥,M). We denote the quotient set S⊥/Eθ by Sθ⊥ and use Sθ to denote the set Sθ⊥∖{⊥Eθ}. Further, we use q,s,t,u,v to denote elements of S⊥ and α,β,γ to denote elements of the ada M.
3.1. Properties of maximal congruences
The following properties are useful in proving the main theorem.
Proposition 3.2**.**
No two elements of {T,F,U} are related under θ. That is, (T,F)∈/θ, (T,U)∈/θ and (F,U)∈/θ.
Proof.
If (T,F)∈θ then we show that θ=M×M; contradicting the maximality of θ. Suppose (T,F)∈θ and let α,β∈M. Then (T,F),(α,α)∈θ⇒(T∧α,F∧α)∈θ that is (α,F)∈θ. Similarly (β,F)∈θ and so using the symmetry and transitivity of θ we have (α,β)∈θ and consequently θ=M×M. The proof of (T,U)∈/θ follows along similar lines. Finally since (F,U)∈θ⇔(T,U)∈θ, the result follows.
∎
Proposition 3.3**.**
For each q∈S⊥, we have
- (i)
(q∘T)[q,⊥]=q.
2. (ii)
(q∘T,F)∈/θ.
3. (iii)
(q∘T,U)∈θ⇔(q,⊥)∈Eθ.
4. (iv)
(q∘T,T)∈θ⇔(q∘F,F)∈θ⇔(q,⊥)∈/Eθ.
5. (v)
(s,t)∈Eθ⇒(s∘α,t∘α)∈θ* for all α∈M.*
6. (vi)
(1,⊥)∈/Eθ.
Proof.
- (i)
Using (44) we have q=q⋅1=q⋅T[1,⊥]=(q∘T)[q⋅1,q⋅⊥]=(q∘T)[q,⊥].
2. (ii)
We prove the result by contradiction. Suppose (q∘T,F)∈θ. Using the fact that θ is a congruence on M and (40) we have (q∘T,F)∈θ⇒(¬(q∘T),¬F)∈θ⇒(q∘(¬T),¬F)∈θ⇒(q∘F,T)∈θ. Similarly using the fact that θ is a congruence, (41) and (40) we have ((q∘F)∨(q∘T),(T∨F))∈θ⇒(q∘(F∨T),(T∨F))∈θ⇒(q∘T,T)∈θ. Thus we have (q∘T,F)∈θ and (q∘T,T)∈θ. From the symmetry and transitivity of θ it follows that (T,F)∈θ, a contradiction by Proposition 3.2. The result follows.
3. (iii)
(⇒:) Let (q∘T,U)∈θ. Using Proposition 1.9(i) we can say that for any choice of s,t∈S⊥ we have ((q∘T)[s,t],⊥)∈Eθ. On choosing s=q,t=⊥ and using Proposition 3.3(i) we have ((q∘T)[q,⊥],⊥)∈Eθ that is (q,⊥)∈Eθ as desired.
(:⇐) First note that, for α∈M,
[TABLE]
(cf. [19, Proposition 2.8(1)]). Now assume that (q,⊥)∈Eθ. Then there exists β∈Tθ such that β[q,⊥]=β[⊥,⊥]. However, by (47), we have β[q,⊥]=⊥. Thus, β[q,⊥]∘T=⊥∘T so that β[[q∘T,⊥∘T]]=U (using (37) and (45)). Consequently, using (47) on (M,M), we have β[[q∘T,U]]=β[[U,U]].
Hence (q∘T,U)∈EθM and so from Proposition 1.9(iii), (q∘T,U)∈θ.
Thus (q∘T,U)∈θ⇔(q,⊥)∈Eθ.
4. (iv)
We first show that (q∘T,T)∈θ⇔(q∘F,F)∈θ by making use of the substitution property of the congruence θ with respect to ¬, the fact that ¬ is an involution and (40). Thus (q∘T,T)∈θ⇔(¬(q∘T),¬T)∈θ⇔(q∘(¬T),¬T)∈θ⇔(q∘F,F)∈θ. Using Proposition 3.2, Proposition 3.3(ii) and Proposition 3.3(iii) we show the equivalence (q∘T,T)∈θ⇔(q,⊥)∈/Eθ. We have (q∘T,T)∈θ⇒(q∘T,U)∈/θ⇒(q,⊥)∈/Eθ. Conversely (q,⊥)∈/Eθ⇒(q∘T,U)∈/θ. Using Proposition 3.3(ii) it follows that (q∘T,F)∈/θ. Since θ is a maximal congruence the only remaining possibility is that (q∘T,T)∈θ which completes the proof.
5. (v)
Consider (s,t)∈Eθ and α∈M. Then there exists β∈Tθ such that β[s,t]=β[t,t]. Thus β[s,t]∘α=β[t,t]∘α. Using (45) we have β[[s∘α,t∘α]]=β[[t∘α,t∘α]] from which it follows that (s∘α,t∘α)∈EθM⊆θ by Proposition 1.9(iii).
6. (vi)
Suppose that (1,⊥)∈Eθ. Using Proposition 3.3(v), (39), (37) we have (1,⊥)∈Eθ⇒(1∘T,⊥∘T)∈θ and so (T,U)∈θ a contradiction by Proposition 3.2.
∎
3.2. A class of homomorphisms separating pairs of elements
For each maximal congruence θ on M, in this subsection, we present homomorphisms ϕθ:S⊥→To(Sθ⊥) and ρθ:M→3Sθ. Then we establish that (ϕθ,ρθ) is a homomorphism from (S⊥,M) to the functional C-monoid \big{(}\mathcal{T}_{o}(S_{{\theta_{\bot}}}),\mathbb{3}^{S_{\theta}}). Further, we ascertain that every pair of elements in S⊥ (or M) are separated by some ϕθ (or ρθ).
Proposition 3.4**.**
The function ϕθ:S⊥→To(Sθ⊥) given by ϕθ(s)=ψθs, where ψθs(tEθ)=t⋅sEθ, is a monoid homomorphism that maps the zero (and base point) of S⊥ to that of To(Sθ⊥), that is ⊥↦ζ⊥.
Proof.
Claim: ϕθ is well-defined. It suffices to show that ψθs is well-defined and that ψθs∈To(Sθ⊥), that is ψθs(⊥)=⊥. In order to show the well-definedness of ψθs we consider u=t that is (u,t)∈Eθ. Then there exists β∈Tθ such that β[u,t]=β[t,t]. Consequently
[TABLE]
Thus (u⋅s,t⋅s)∈Eθ and so ψθs(u)=ψθs(t). Also ψθs(⊥)=⊥⋅s=⊥. Thus ψθs∈To(Sθ⊥).
Claim: ϕθ(⊥)=ζ⊥ . We have ϕθ(⊥)=ψθ⊥ where ψθ⊥(t)=t⋅⊥=⊥. Thus ϕθ(⊥)=ζ⊥.
Claim: ϕθ(1)=idSθ⊥. We have ϕθ(1)=ψθ1 where ψθ1(t)=t⋅1=t.
Claim: ϕθ is a semigroup homomorphism. Consider ϕθ(s⋅t)=ψθs⋅t where ψθs⋅t(u)=u⋅(s⋅t)=(u⋅s)⋅t=ψθt(u⋅s)=ψθt(ψθs(u))=(ψθs⋅ψθt)(u). Thus ϕθ(s⋅t)=ϕθ(s)⋅ϕθ(t).
∎
Proposition 3.5**.**
The function ρθ:M→3Sθ given by
[TABLE]
where Aθα={tEθ:t∘α∈Tθ} and Bθα={tEθ:t∘α∈Fθ}, is a homomorphism of C-algebras with T,F,U.
Proof.
Claim: ρθ is well-defined. If α∈{T,F} then the proof is obvious. If α∈/{T,F} then we show that Aθα∩Bθα=∅ and that Aθα,Bθα⊆Sθ, that is, ⊥∈/Aθα∪Bθα. Let t∈Aθα∩Bθα. Then t∘α∈Tθ and t∘α∈Fθ and so (T,F)∈θ which is a contradiction to Proposition 3.2. Using (37) we have ⊥∘α=U and so if ⊥∈Aθα∪Bθα we would have ⊥∘α=U∈{Tθ,Fθ}, a contradiction to Proposition 3.2. Finally we show that the image under ρθ is independent of the representative of the equivalence class chosen. Using Proposition 3.3(v) we have s=t⇒(s∘α,t∘α)∈θ. The result follows.
Claim: ρθ preserves the constants T,F,U. It is clear that ρθ(T)=(Sθ,∅), ρθ(F)=(∅,Sθ) and, using (38) and Proposition 3.2, that ρθ(U)=(AθU,BθU)=(∅,∅) from which the result follows.
Claim: ρθ is a C-algebra homomorphism. We show that ρθ(¬α)=¬(ρθ(α)). If α∈{T,F} the proof is obvious. Suppose that α∈/{T,F}. Then we have the following.
[TABLE]
Finally we show that ρθ(α∧β)=ρθ(α)∧ρθ(β). Note that the proof of ρθ(α∨β)=ρθ(α)∨ρθ(β) follows using the double negation and De Morgan’s laws, viz., (15) and (16) respectively in conjunction with the fact that ρθ preserves ¬ and ∧. In order to prove that ρθ(α∧β)=ρθ(α)∧ρθ(β) we proceed by considering the following cases.
Case I: α,β∈/{T,F}. We have the following subcases:
Subcase 1: α∧β∈/{T,F}. Then ρθ(α∧β)=(Aθα∧β,Bθα∧β), ρθ(α)=(Aθα,Bθα) and ρθ(β)=(Aθβ,Bθβ). Now (Aθα,Bθα)∧(Aθβ,Bθβ)=(Aθα∩Aθβ,Bθα∪(Aθα∩Bθβ)). Thus we have to show that
[TABLE]
We show that the pairs of sets are equal componentwise.
Let q∈Aθα∧β. Then q∘(α∧β)∈Tθ
[TABLE]
so that q∈Aθα. Along similar lines one can observe that
[TABLE]
Consequently (q∘β,T)∈θ so that q∈Aθβ. Hence Aθα∧β⊆Aθα∩Aθβ.
For reverse inclusion let q∈Aθα∩Aθβ. Then (q∘α,T),(q∘β,T)∈θ. Since θ is a congruence we have ((q∘α)∧(q∘β),T∧T)=((q∘α)∧(q∘β),T)=((q∘(α∧β),T)∈θ and so q∈Aθα∧β. Hence Aθα∧β=Aθα∩Aθβ.
In order to show that Bθα∧β⊆Bθα∪(Aθα∩Bθβ) consider q∈Bθα∧β that is (q∘(α∧β),F)∈θ. Since θ is a maximal congruence consider the following three possibilities:
(q∘α,F)∈θ**: **
Then clearly q∈Bθα and so q∈Bθα∪(Aθα∩Bθβ).
(q∘α,T)∈θ**: **
Then we have q∈Aθα. We show that (q∘β,F)∈θ. If this is not the case then either (q∘β,T)∈θ or (q∘β,U)∈θ. If (q∘β,T)∈θ then since (q∘α,T)∈θ we have (q∘(α∧β),T∧T)=(q∘(α∧β),T)∈θ using (41) and the fact that θ is a congruence. However since (q∘(α∧β),F)∈θ we obtain a contradiction that (T,F)∈θ (cf. Proposition 3.2). Along similar lines if (q∘β,U)∈θ then as (q∘α,T)∈θ we have (q∘(α∧β),U)∈θ and so (F,U)∈θ a contradiction to Proposition 3.2. Hence (q∘β,F)∈θ so that q∈(Aθα∩Bθβ)⊆Bθα∪(Aθα∩Bθβ).
(q∘α,U)∈θ**: **
Since (q∘β,q∘β)∈θ we have (q∘(α∧β),U∧q∘β)=(q∘(α∧β),U)∈θ using (41) and the fact that θ is a congruence. However since (q∘(α∧β),F)∈θ we have (F,U)∈θ a contradiction to Proposition 3.2. Thus this case cannot occur.
To show the reverse inclusion let q∈Bθα∪(Aθα∩Bθβ) that is q∈Bθα or q∈Aθα∩Bθβ.
If q∈Bθα then (q∘α,F)∈θ
[TABLE]
from which it follows that q∈Bθα∧β. In the case where q∈Aθα∩Bθβ that is (q∘α,T),(q∘β,F)∈θ, along similar lines it follows that (q∘(α∧β),T∧F)=(q∘(α∧β),F)∈θ and so q∈Bθα∧β. Therefore Bθα∧β=Bθα∪(Aθα∩Bθβ).
Subcase 2: α∧β∈{T,F}. Using the fact that M≤3X for some set X it is easy to see that if α,β∈/{T,F} then α∧β=T. It follows that the only possibility in this case is that α∧β=F. Therefore ρθ(α∧β)=ρθ(F)=(∅,Sθ) and ρθ(α)∧ρθ(β)=(Aθα∩Aθβ,Bθα∪(Aθα∩Bθβ)) and so we have to show that
[TABLE]
We first show that Aθα∩Aθβ=∅. If Aθα∩Aθβ=∅ then let q∈Aθα∩Aθβ so that (q∘α,T)∈θ,(q∘β,T)∈θ
[TABLE]
which is a contradiction to Proposition 3.3(ii). Hence Aθα∩Aθβ=∅.
In order to show that Bθα∪(Aθα∩Bθβ)=Sθ consider q∈Sθ that is q=⊥ which gives (q,⊥)∈/Eθ. We proceed by considering the following three cases:
(q∘α,F)∈θ**: **
Then it is clear that q∈Bθα⊆Bθα∪(Aθα∩Bθβ).
(q∘α,T)∈θ**: **
Then we have q∈Aθα. We show that (q∘β,F)∈θ. Suppose that this is not the case. Since θ is a maximal congruence it implies that either (q∘β,T)∈θ or (q∘β,U)∈θ. If (q∘β,T)∈θ then since (q∘α,T)∈θ it follows that (q∘(α∧β),T∧T)=(q∘F,T)∈θ so that (q∘T,F)∈θ. This is a contradiction to Proposition 3.3(ii). In the case that (q∘β,U)∈θ proceeding as earlier we have (q∘(α∧β),T∧U)=(q∘F,U)∈θ so that (q∘T,U)∈θ. It follows from Proposition 3.3(iii) that (q,⊥)∈Eθ which is a contradiction to the assumption that q∈Sθ. Consequently it must be the case that (q∘β,F)∈θ so that q∈Aθα∩Bθβ⊆Bθα∪(Aθα∩Bθβ).
(q∘α,U)∈θ**: **
Since θ is a congruence we have (q∘β,q∘β)∈θ
[TABLE]
Thus using Proposition 3.3(iii) we have (q,⊥)∈Eθ which is a contradiction to the assumption that q∈Sθ. Hence this case cannot occur.
Thus Bθα∪(Aθα∩Bθβ)=Sθ which completes the proof in the case where α,β∈/{T,F}.
Case II: α∈{T,F}. The verification is straightforward by considering α=T and α=F casewise.
Subcase 1: α=T. Then ρθ(α∧β)=ρθ(T∧β)=ρθ(β)=(Sθ,∅)∧ρθ(β)=ρθ(T)∧ρθ(β)=ρθ(α)∧ρθ(β).
Subcase 2: α=F. Then ρθ(α∧β)=ρθ(F∧β)=ρθ(F)=(∅,Sθ)=(∅,Sθ)∧ρθ(β)=ρθ(F)∧ρθ(β)=ρθ(α)∧ρθ(β).
Case III: β∈{T,F}. We have the following subcases:
Subcase 1: β=T. The proof follows along the same lines as Case II above since T is the left and right-identity for ∧. Thus ρθ(α∧β)=ρθ(α∧T)=ρθ(α)=ρθ(α)∧(Sθ,∅)=ρθ(α)∧ρθ(T)=ρθ(α)∧ρθ(β).
Subcase 2: β=F. If α∈{T,F} then this reduces to Case II proved above and consequently we have ρθ(α∧β)=ρθ(α)∧ρθ(β) in this case. Thus it remains to consider the case where α∈/{T,F}. We then have the following subcases depending on α∧β:
α∧β∈/{T,F}**: **
Then ρθ(α∧β)=ρθ(α∧F)=(Aθα∧F,Bθα∧F) while ρθ(α)=(Aθα,Bθα) and ρθ(β)=ρθ(F)=(∅,Sθ). Thus ρθ(α)∧ρθ(F)=(∅,Aθα∪Bθα). We show that
[TABLE]
as earlier by proving that the pairs of sets are equal componentwise.
We show that Aθα∧F=∅ by contradiction. If Aθα∧F=∅ then consider q∈Aθα∧F. It follows that (q∘(α∧F),T)∈θ
[TABLE]
which is a contradiction to Proposition 3.3(ii). Hence Aθα∧F=∅.
We show that Bθα∧F=Aθα∪Bθα using standard set theoretic arguments. Let q∈Bθα∧F and so (q∘(α∧F),F)∈θ so that ((q∘α)∧(q∘F),F)∈θ. In view of the maximality of θ it suffices to consider three cases. If either (q∘α,T)∈θ or (q∘α,F)∈θ then q∈Aθα∪Bθα. If (q∘α,U)∈θ then ((q∘α)∧((q∘α)∧(q∘F)),U∧F)=((q∘α)∧(q∘F),U)∈θ.Thus (F,U)∈θ which is a contradiction to Proposition 3.2. Hence this case cannot occur and so Bθα∧F⊆Aθα∪Bθα.
For the reverse inclusion consider q∈Aθα∪Bθα so that q∈Aθα or q∈Bθα. If q∈Aθα then (q∘α,T)∈θ. Since q∈Aθα⊆Sθ using Proposition 3.3(iv) we have (q,⊥)∈/Eθ⇒(q∘F,F)∈θ. Consequently (q∘(α∧F),(T∧F))=(q∘(α∧F),F)∈θ and so q∈Bθα∧F. Along similar lines if q∈Bθα we have (q∘(α∧F),F)∈θ so that q∈Bθα∧F. Hence (Aθα∧F,Bθα∧F)=(∅,Aθα∪Bθα).
α∧β∈{T,F}**: **
Using the fact that M≤3X for some set X we have α∧F=T from which it follows that the only case is α∧β=α∧F=F. Thus ρθ(α∧F)=ρθ(F)=(∅,Sθ) while ρθ(α)∧ρθ(F)=(∅,Aθα∪Bθα). We show that
[TABLE]
In order to show that Aθα∪Bθα=Sθ consider q∈Sθ. If (q∘α,T)∈θ or (q∘α,F)∈θ then the proof is complete. If (q∘α,U)∈θ then since q=⊥ that is (q,⊥)∈/Eθ by Proposition 3.3(iv) we have (q∘F,F)∈θ. Thus (q∘(α∧F),U∧F)=(q∘F,U)∈θ. Consequently from the transitivity of θ it follows that (F,U)∈θ which is a contradiction to Proposition 3.2. Hence (∅,Sθ)=(∅,Aθα∪Bθα).
Thus ρθ is a homomorphism of C-algebras with T,F,U.
∎
Lemma 3.6**.**
The pair (ϕθ,ρθ) is a C-monoid homomorphism from (S⊥,M) to the functional C-monoid \big{(}\mathcal{T}_{o}(S_{{\theta_{\bot}}}),\mathbb{3}^{S_{\theta}}\big{)}.
Proof.
In view of Proposition 3.4 and Proposition 3.5 it suffices to show that ϕθ(α[s,t])=ρθ(α)[ϕθ(s),ϕθ(t)] and ρθ(s∘α)=ϕθ(s)∘ρθ(α) hold. In order to show that ϕθ(α[s,t])=ρθ(α)[ϕθ(s),ϕθ(t)] we proceed casewise depending on the value of α as per the following:
Case I: α∈{T,F}. If α=T then ϕθ(α[s,t])=ϕθ(T[s,t])=ϕθ(s)=(Sθ,∅)[ϕθ(s),ϕθ(t)]=ρθ(T)[ϕθ(s),ϕθ(t)]=ρθ(α)[ϕθ(s),ϕθ(t)]. Along similar lines if α=F then ϕθ(α[s,t])=ϕθ(F[s,t])=ϕθ(t)=(∅,Sθ)[ϕθ(s),ϕθ(t)]=ρθ(F)[ϕθ(s),ϕθ(t)]=ρθ(α)[ϕθ(s),ϕθ(t)].
Case II: α∈/{T,F}. If α∈/{T,F} then using (44) we have ϕθ(α[s,t])=ψθα[s,t] where ψθα[s,t](v)=v⋅(α[s,t])=(v∘α)[v⋅s,v⋅t]. Consider ρθ(α)[ϕθ(s),ϕθ(t)]=(Aθα,Bθα)[ψθs,ψθt], where
[TABLE]
It suffices to consider the following three cases:
Subcase 1: (v∘α)∈Tθ. using Proposition 1.9(i) we have ((v∘α)[v⋅s,v⋅t],v⋅s)∈Eθ. Consequently (v∘α)[v⋅s,v⋅t]=v⋅s.
Subcase 2: (v∘α)∈Fθ. Along similar lines if (v∘α)∈Fθ then ((v∘α)[v⋅s,v⋅t],v⋅t)∈Eθ, by Proposition 1.9(i) and so (v∘α)[v⋅s,v⋅t]=v⋅t.
Subcase 3: (v∘α)∈Uθ. Then ((v∘α)[v⋅s,v⋅t],⊥)∈Eθ, by Proposition 1.9(i) which gives (v∘α)[v⋅s,v⋅t]=⊥.
Thus we have ψθα[s,t](v)=(Aθα,Bθα)[ψθs,ψθt](v) for every v∈Sθ⊥ and so ϕθ(α[s,t])=ρθ(α)[ϕθ(s),ϕθ(t)].
We show that ρθ(s∘α)=ϕθ(s)∘ρθ(α) by proceeding casewise depending on the value of α and s∘α.
Case I: α∈/{T,F},s∘α∈/{T,F}. Then ρθ(s∘α)=(Aθs∘α,Bθs∘α) and ρθ(α)=(Aθα,Bθα). Then ϕθ(s)∘(Aθα,Bθα)=ψθs∘(Aθα,Bθα)=(C,D), where C={q∈Sθ:ψθs(q)∈Aθα} and D={q∈Sθ:ψθs(q)∈Bθα}. We have to show that
[TABLE]
It is clear that q∈C
[TABLE]
Along similar lines we have q∈D⇔q∈Bθs∘α.
Case II: α∈{T,F},s∘α∈/{T,F}. If α=T then ρθ(s∘α)=ρθ(s∘T)=(Aθs∘T,Bθs∘T). On the other hand ϕθ(s)∘ρθ(α)=ϕθ(s)∘ρθ(T)=ψθs∘(Sθ,∅)=(C,D) where C={q∈Sθ:ψθs(q)∈Sθ} and D=∅. We have to show that
[TABLE]
We show that Bθs∘T=∅ by contradiction. If Bθs∘T=∅ then let q∈Bθs∘T
[TABLE]
which is a contradiction to Proposition 3.3(ii). Thus Bθs∘T=∅.
We now show that Aθs∘T=C. It is clear that q∈C
[TABLE]
In the case where α=F the proof follows along similar lines.
Case III: α∈/{T,F},s∘α∈{T,F}. We have the following subcases:
Subcase 1: s∘α=T. Then ρθ(s∘α)=ρθ(T)=(Sθ,∅). On the other hand ϕθ(s)∘ρθ(α)=ψθs∘(Aθα,Bθα)=(C,D) where C={q∈Sθ:ψθs(q)∈Aθα} and D={q∈Sθ:ψθs(q)∈Bθα}. We have to show that
[TABLE]
We first show by contradiction that D=∅. If D=∅ consider q∈D
[TABLE]
which is a contradiction to Proposition 3.3(ii).
In order to show that C=Sθ consider q∈Sθ that is (q,⊥)∈/Eθ
[TABLE]
Subcase 2: s∘α=F. Then ρθ(s∘α)=ρθ(F)=(∅,Sθ) while ϕθ(s)∘ρθ(α)=ψθs∘(Aθα,Bθα)=(C,D) where C={q∈Sθ:ψθs(q)∈Aθα} and D={q∈Sθ:ψθs(q)∈Bθα}. We have to show that
[TABLE]
We first show C=∅ by contradiction. If C=∅ consider q∈C
[TABLE]
which is a contradiction to Proposition 3.3(ii).
In order to show that D=Sθ consider q∈Sθ that is (q,⊥)∈/Eθ.
[TABLE]
which completes the proof for the case where α∈/{T,F} and s∘α∈{T,F}.
Case IV: α∈{T,F},s∘α∈{T,F}. Note that s∘T=F as a consequence of Proposition 3.3(ii). If s∘T=F then as θ is a congruence, (F,F)∈θ⇒(s∘T,F)∈θ, a contradiction to Proposition 3.3(ii). Similarly we have s∘F=T. In view of the above it suffices to consider the following cases:
Subcase 1: α=T,s∘α=T. Then ρθ(s∘α)=ρθ(T)=(Sθ,∅) and ϕθ(s)∘ρθ(α)=ψθs∘(Sθ,∅)=(C,D) where C={q∈Sθ:ψθs(q)∈Sθ} and D=∅. Thus it suffices to show that C=Sθ. Let q∈Sθ that is (q,⊥)∈/Eθ
[TABLE]
Thus C=Sθ.
Subcase 2: α=F,s∘α=F. Then ρθ(s∘α)=ρθ(F)=(∅,Sθ) and ϕθ(s)∘ρθ(α)=ψθs∘(∅,Sθ)=(C,D) where C=∅ and D={q∈Sθ:ψθs(q)∈Sθ}. The proof follows along similar lines as above. In order to show that D=Sθ consider q∈Sθ that is (q,⊥)∈/Eθ
[TABLE]
Hence D=Sθ which completes the proof.
Thus (ϕθ,ρθ) is a homomorphism of C-monoids.
∎
Proposition 3.7**.**
For all α∈M the following statements hold:
- (i)
ρθ(α)=(Sθ,∅)⇒(α,T)∈θ.
2. (ii)
ρθ(α)=(∅,Sθ)⇒(α,F)∈θ.
Proof.
- (i)
If α=T then the result is obvious. Suppose that α=T and ρθ(α)=(Aθα,Bθα)=(Sθ,∅). It follows that (t∘α,T)∈θ for all t∈Sθ. Using Proposition 3.3(vi) and (39) we have 1∈Sθ and so (1∘α,T)=(α,T)∈θ.
2. (ii)
Along similar lines if α=F then ρθ(α)=(Aθα,Bθα)=(∅,Sθ) gives (t∘α,F)∈θ for all t∈Sθ. Using Proposition 3.3(vi) and (39) we have 1∈Sθ and so (1∘α,F)=(α,F)∈θ.
∎
Lemma 3.8**.**
For every s,t∈S⊥ where s=t there exists a maximal congruence θ on M such that ϕθ(s)=ϕθ(t).
Proof.
Using Proposition 1.9(iv) we have ⋂Eθ=ΔS⊥ and so since s=t there exists a maximal congruence θ on M such that (s,t)∈/Eθ, i.e., s=t. For this θ, consider ϕθ:S⊥→To(Sθ⊥). Then ϕθ(s)=ψθs, ϕθ(t)=ψθt. For 1∈Sθ⊥ we have ψθs(1)=1⋅s=s while ψθt(1)=1⋅t=t. Since s=t it follows that ϕθ(s)=ϕθ(t).
∎
Lemma 3.9**.**
For every α,β∈M where α=β there exists a maximal congruence θ on M such that ρθ(α)=ρθ(β).
Proof.
Using Proposition 1.9(v) since α=β there exists a maximal congruence θ on M such that (α,β)∈/θ. We show that ρθ(α)=ρθ(β). If α or β is in {T,F} but ρθ(α)=ρθ(β) then using Proposition 3.7 we have (α,β)∈θ, a contradiction. In the case where α,β∈/{T,F} we show that
[TABLE]
by showing that either Aθα=Aθβ or that Bθα=Bθβ. Owing to Proposition 3.2 it suffices to consider the following three cases:
Case I: (α,T)∈θ. Note that Proposition 3.3(vi) gives 1∈Sθ. Thus we have 1∈Sθ for which 1∘α=α∈Tθ and so 1∈Aθα. However 1∈/Aθβ since (α,β)∈/θ.
Case II: (α,F)∈θ. Along similar lines for 1∈Sθ we have 1∘α=α∈Fθ and so 1∈Bθα. It is clear that 1∈/Bθβ since (α,β)∈/θ.
Case III: (α,U)∈θ. In view of Proposition 3.2 it suffices to consider the following cases:
Subcase 1: (β,T)∈θ. As earlier we have 1∈Aθβ∖Aθα.
Subcase 2: (β,F)∈θ. It is clear that 1∈Bθβ∖Bθα.
Thus ρθ(α)=ρθ(β) which completes the proof.
∎
3.3. Embedding into a functional C-monoid
Let {θ} be the collection of all maximal congruences of M. Define the set X to be the disjoint union of Sθ taken over all maximal congruences of M, written
[TABLE]
Set X⊥=X∪{⊥} with base point ⊥∈/X. For notational convenience we use the same symbol ⊥ in X⊥ as well as in S⊥. Which ⊥ we are referring to will be clear from the context of the statement.
In this subsection we obtain monomorphisms ϕ:S⊥→To(X⊥) and ρ:M→3X, using which we establish that (S⊥,M) can be embedded into the functional C-monoid \big{(}\mathcal{T}_{o}(X_{\bot}),\mathbb{3}^{X}\big{)}.
Remark 3.10*.*
- (i)
Let q∈S be fixed. For different θ’s the representation of classes qEθ’s are different in the disjoint union X of Sθ’s.
2. (ii)
Let {Aλ},{Bλ} be two families of sets indexed over Λ. Then \displaystyle\bigsqcup_{\lambda}(A_{\lambda}\cap B_{\lambda})=\Big{(}\bigsqcup_{\lambda}A_{\lambda}\Big{)}\cap\Big{(}\bigsqcup_{\lambda}B_{\lambda}\Big{)} and \displaystyle\bigsqcup_{\lambda}(A_{\lambda}\cup B_{\lambda})=\Big{(}\bigsqcup_{\lambda}A_{\lambda}\Big{)}\cup\Big{(}\bigsqcup_{\lambda}B_{\lambda}\Big{)}.
Notation 3.11**.**
- (i)
For the pair of sets (A,B), we denote by π1(A,B) the first component A, and by π2(A,B) the second component B.
2. (ii)
For a family of pairs of sets (Aλ,Bλ) where λ∈Λ we denote by λ⨆(Aλ,Bλ) the pair of sets \displaystyle\Big{(}\bigsqcup_{\lambda}A_{\lambda},\bigsqcup_{\lambda}B_{\lambda}\Big{)}.
Lemma 3.12**.**
Consider ϕ:S⊥→To(X⊥) given by
[TABLE]
Then ϕ is a monoid monomorphism that maps the zero (and base point) of S⊥ to that of To(X⊥), that is ⊥↦ζ⊥.
Proof.
It is clear that ϕ is well-defined and that ϕ(s)∈To(X⊥) since (ϕ(s))(⊥)=⊥.
Claim: ϕ is injective. Let s=t∈S⊥. Using Lemma 3.8 there exists a maximal congruence θ on M such that ϕθ(s)=ϕθ(t). Hence there exists a qEθ(=⊥Eθ) such that (ϕθ(s))(q)=(ϕθ(t))(q). By extrapolation it follows that (ϕ(s))(q)=(ϕ(t))(q) and so ϕ(s)=ϕ(t).
Claim: ϕ(⊥)=ζ⊥. Using Proposition 3.4 we have ϕθ(⊥)=ζ⊥Eθ for all θ and so by definition (ϕ(⊥))(x)=⊥ for all x∈X⊥.
Claim: ϕ(1)=idX⊥. It is clear that (ϕ(1))(⊥)=⊥. Consider q∈X that is qEθ∈Sθ for some θ. Then by Proposition 3.4 we have (ϕ(1))(qEθ)=(ϕθ(1))(qEθ)=qEθ and hence ϕ(1)=idX⊥.
Claim: ϕ(s⋅t)=ϕ(s)⋅ϕ(t). Clearly (ϕ(s⋅t))(⊥)=⊥=(ϕ(s)⋅ϕ(t))(⊥). Let q∈X that is qEθ∈Sθ for some θ. Suppose that (ϕ(s⋅t))(q)=⊥ so that (ϕθ(s⋅t))(q)=⊥
[TABLE]
Noting that there are only two possibilities for ϕ(s)(q) we see that if ϕ(s)(q)=ϕθ(s)(q) then we are through. On the other hand if ϕ(s)(q)=⊥ that is ϕθ(s)(q)=⊥ then we have (ϕ(s⋅t))(q)=⊥=(ϕ(s)⋅ϕ(t))(q) which completes the proof in this case.
Consider the case where (ϕ(s⋅t))(q)=⊥. Using Proposition 3.4 it follows that (ϕ(s⋅t))(q)=(ϕθ(s⋅t))(q)=(ϕθ(s)⋅ϕθ(t))(q)=ϕθ(t)(ϕθ(s)(q)) and so (ϕθ(s))(q)=⊥. Consequently ϕ(t)(ϕ(s)(q))=ϕθ(t)(ϕθ(s)(q)) since (ϕθ(s))(q)=⊥. It follows that (ϕ(s⋅t))(q)=(ϕ(s)⋅ϕ(t))(q) which completes the proof.
∎
Lemma 3.13**.**
The function ρ:M→3X defined by
[TABLE]
is a monomorphism of C-algebras with T,F,U.
Proof.
Claim: ρ is well defined. Let α∈M. Using Remark 3.10(i) we have π1(ρ(α))∩π2(ρ(α))=∅ due to the distinct representation of equivalence classes. Also by Proposition 3.5 we have π1(ρθ(α)),π2(ρθ(α))⊆Sθ and so ⊥∈/π1(ρ(α))∪π2(ρ(α)) that is ρ(α) is can be identified with a pair of sets over X.
Claim: ρ is injective. Let α=β∈M. By Lemma 3.9 there exists a θ such that ρθ(α)=ρθ(β). Without loss of generality we infer that there exists a qEθ∈π1(ρθ(α))∖π1(ρθ(β)). Since ρ(α) is formed by taking the disjoint union of the individual images under ρθ(α), using Remark 3.10(i) we can say that q∈π1(ρ(α))∖π1(ρ(β)) that is ρ(α)=ρ(β).
Claim: ρ preserves the constants T,F,U. It follows easily from Proposition 3.5 that ρ(T)=(X,∅), ρ(F)=(∅,X) and ρ(U)=(∅,∅).
Claim: ρ(¬α)=¬(ρ(α)). If α∈{T,F} then the result is obvious. If α∈/{T,F} then ¬α∈/{T,F}. Using Proposition 3.5 we have ρ(¬α)=(⊔Aθ¬α,⊔Bθ¬α)=(⊔Bθα,⊔Aθα). Thus ρ(¬α)=(⊔Bθα,⊔Aθα)=¬(ρ(α)).
Claim: ρ(α∧β)=ρ(α)∧ρ(β). In view of Remark 3.10(ii) we have ⊔((Aλ,Bλ)∧(Cλ,Dλ))=(⊔Aγ,⊔Bγ)∧(⊔Cγ,⊔Dγ) for the family of pairs of sets (Aλ,Bλ),(Cλ,Dλ) where λ∈Λ over X. In view of the above and Proposition 3.5 we have ⊔ρθ(α∧β)=⊔(ρθ(α)∧ρθ(β))=(⊔ρθ(α))∧(⊔ρθ(β))=ρ(α)∧ρ(β) which completes the proof.
∎
Lemma 3.14**.**
The pair (ϕ,ρ) is a C-monoid monomorphism from (S⊥,M) to the functional C-monoid \big{(}\mathcal{T}_{o}(X_{\bot}),\mathbb{3}^{X}\big{)}.
Proof.
In view of Lemma 3.12 and Lemma 3.13 it suffices to show ϕ(α[s,t])=(ρ(α))[ϕ(s),ϕ(t)] and ρ(s∘α)=ϕ(s)∘ρ(α).
In order to show that ϕ(α[s,t])=(ρ(α))[ϕ(s),ϕ(t)] we show that ϕ(α[s,t])(x)=(ρ(α))[ϕ(s),ϕ(t)](x) for all x∈X⊥. Thus we have the following cases:
Case I: x=⊥. It is clear that ϕ(α[s,t])(⊥)=⊥=(ρ(α))[ϕ(s),ϕ(t)](⊥) since π1(ρ(α)),π2(ρ(α))⊆X and ⊥∈/X.
Case II: x∈X. Consider q∈X that is qEθ∈Sθ for some θ. We have the following subcases:
Subcase 1: ϕ(α[s,t])(q)=⊥. then ϕθ(α[s,t])(q)=⊥ and so using Lemma 3.6 we have ϕθ(α[s,t])(q)=⊥=(ρθ(α))[ϕθ(s),ϕθ(t)](q). It follows that either q∈/π1(ρθ(α))∪π2(ρθ(α)) or that q∈π1(ρθ(α)) and ϕθ(s)(q)=⊥ or, similarly, that q∈π2(ρθ(α)) and ϕθ(t)(q)=⊥. Thus we have the following:
q∈/π1(ρθ(α))∪π2(ρθ(α))**: **
In view of Remark 3.10(i) it follows that q∈/π1(ρ(α))∪π2(ρ(α)) and so (ρ(α))[ϕ(s),ϕ(t)](q)=⊥.
q∈π1(ρθ(α))** and ϕθ(s)(q)=⊥: **
Then q∈π1(ρ(α)) and ϕ(s)(q)=⊥ and so (ρ(α))[ϕ(s),ϕ(t)](q)=⊥.
q∈π2(ρθ(α))** and ϕθ(t)(q)=⊥: **
Along similar lines we have (ρ(α))[ϕ(s),ϕ(t)](q)=⊥.
Subcase 2: ϕ(α[s,t])(q)=⊥. Then ϕ(α[s,t])(q)=ϕθ(α[s,t])(q) and so using Lemma 3.6 we have ϕ(α[s,t])(q)=(ρθ(α))[ϕθ(s),ϕθ(t)](q). It follows that
[TABLE]
q∈π1(ρθ(α))**: **
It follows that q∈π1(ρ(α)) and so (ρ(α))[ϕ(s),ϕ(t)](q)=ϕ(s)(q). Note that ϕθ(s)(q)=⊥ else ϕ(α[s,t])(q)=⊥, a contradiction. Thus ϕ(s)(q)=ϕθ(s)(q) so that ϕ(α[s,t])(q)=(ρ(α))[ϕ(s),ϕ(t)](q).
q∈π2(ρθ(α))**: **
The proof follows along similar lines as above.
q∈/(π1(ρθ(α))∪π2(ρθ(α)))**: **
This case cannot occur since we assumed that ϕ(α[s,t])(q)=⊥.
Thus ϕ(α[s,t])=(ρ(α))[ϕ(s),ϕ(t)].
We now show that ρ(s∘α)=ϕ(s)∘ρ(α). In order to prove this we proceed by showing that
[TABLE]
for i∈{1,2}.
Let q∈π1(ρ(s∘α))=⊔π1(ρθ(s∘α)). Then qEθ∈Sθ for some θ and qEθ∈π1(ρθ(s∘α))
[TABLE]
and so π1(ρ(s∘α))⊆π1(ϕ(s)∘ρ(α)).
For the reverse inclusion assume that q∈π1(ϕ(s)∘ρ(α)). Consequently we have qEθ∈Sθ for some θ and ϕ(s)(qEθ)∈π1(ρ(α))⊆X
[TABLE]
from which it follows that π1(ϕ(s)∘ρ(α))⊆π1(ρ(s∘α)).
Proceeding along exactly the same lines we can show that π2(ρ(s∘α))=π2(ϕ(s)∘ρ(α)) which completes the proof.
∎
3.4. Proof of Theorem 3.1
Let {θ} be the collection of all maximal congruences of M. Consider the set X as in (48). The functions ϕ:S⊥→To(X⊥) and ρ:M→3X as defined in Lemma 3.12 and Lemma 3.13, respectively, are monomorphisms. Further, by Lemma 3.14, the pair (ϕ,ρ) is a monomorphism from (S⊥,M) to the functional C-monoid \big{(}\mathcal{T}_{o}(X_{\bot}),\mathbb{3}^{X}\big{)}. From the construction of X it is also evident that if M and S⊥ are finite then there are only finitely many maximal congruences θ on M and finitely many equivalence classes Eθ on S⊥ and so X must be finite.
Corollary 3.15**.**
An identity is satisfied in every C-monoid (S⊥,M) where M is an ada if and only if it is satisfied in all functional C-monoids.
In view of Corollary 3.15 and (36), we have the following result.
Corollary 3.16**.**
*In every C-monoid (S⊥,M) where M is an ada we have
(f∘T)[f,f]=f.*
4. Conclusion
The notion of C-sets axiomatize the program construct if-then-else considered over possibly non-halting programs and non-halting tests. In this work, we extended the axiomatization to C-monoids which include the composition of programs as well as composition of programs with tests. For the class of C-monoids where the C-algebra is an ada we obtain a Cayley-type theorem which exhibits the embedding of such C-monoids into functional C-monoids. Using this, we obtain a mechanism to determine the equivalence of programs through functional C-monoids. It is desirable to achieve such a representation for the general class of C-monoids with no restriction on the C-algebra, which can be considered as future work. Note that the term f∘T in the standard functional model of a C-monoid represents the aspect of the domain of the function, as used in [4, 11]. It is interesting to study the relation between these two concepts in the current set up.
Appendix A Proofs
A.1. Verification of Example 2.2
We use the pairs of sets representation given by Guzmán and Squier in [6] and identify α∈3X with a pair of sets (A,B) of X where A=α−1(T) and B=α−1(F). In this representation T=(X,∅),F=(∅,X) and U=(∅,∅). Thus the operation ∘ is given as follows:
[TABLE]
In other words f∘α can be identified with the pair of sets (C,D) where C={x∈X:f(x)∈A} and D={x∈X:f(x)∈B}.
Axiom (37): Let α be identified with the pair of sets (A,B). Then ζ⊥∘α=(∅,∅)=U as ζ⊥(x)=⊥∈/(A∪B).
Axiom (38): Consider U=(∅,∅). Then f∘U=(∅,∅)=U.
Axiom (39):
[TABLE]
Thus 1∘α=α.
Axiom (40): Let α be identified with the pair of sets (A,B). Then f∘α=(C,D) where C={x∈X:f(x)∈A} and D={x∈X:f(x)∈B}. Thus ¬(f∘α)=(D,C). Also f∘(¬α)=f∘(B,A)=(E,F) where E={x∈X:f(x)∈B} and F={x∈X:f(x)∈A}. It follows that (E,F)=(D,C).
Axiom (41): Let α,β be represented by the pairs of sets (A1,A2) and (B1,B2) respectively. Then α∧β=(A1∩B1,A2∪(A1∩B2)). Also let f∘α=(C1,C2) where C1={x∈X:f(x)∈A1} and C2={x∈X:f(x)∈A2}, and f∘β=(D1,D2) where D1={x∈X:f(x)∈B1} and D2={x∈X:f(x)∈B2}. Then (C1,C2)∧(D1,D2)=(C1∩D1,C2∪(C1∩D2)). Thus C1∩D1={x∈X:f(x)∈A1∩B1} and C2∪(C1∩D2)={x∈X:f(x)∈A2∪(A1∩B2)}. Hence f∘(α∧β)=(f∘α)∧(f∘β).
Axiom (42): Consider f,g∈To(X⊥) and α∈3X represented by the pair of sets (A,B).
[TABLE]
Let g∘α=(C,D) where C={x∈X:g(x)∈A} and D={x∈X:g(x)∈B}.
[TABLE]
We may consider the following three cases.
Case I: x∈X such that g(f(x))∈A: Then ((f⋅g)∘α)(x)=T. Also f(x)∈C as g(f(x))∈A. Thus (f∘(g∘α))(x)=T.
Case II: x∈X such that g(f(x))∈B: Then ((f⋅g)∘α)(x)=F. Similarly g(f(x))∈B means that f(x)∈D. Thus (f∘(g∘α))(x)=F.
Case III: x∈X such that g(f(x))∈/(A∪B): Then ((f⋅g)∘α)(x)=U. Since f(x) is in neither C nor D it follows that (f∘(g∘α))(x)=U.
Axiom (43): Consider α∈3X represented by the pair of sets (A,B).
[TABLE]
Hence α[f,g]⋅h=α[f⋅h,g⋅h].
Axiom (44): Let α∈3X be represented by the pair of sets (A,B).
[TABLE]
Let h∘α be represented by the pair of sets (C,D) where C={x∈X:h(x)∈A} and D={x∈X:h(x)∈B}.
[TABLE]
Thus h⋅α[f,g]=(h∘α)[h⋅f,h⋅g].
Axiom (45): Let α,β∈3X be represented by the pairs of sets (A1,A2) and (B1,B2) respectively. For f,g∈To(X⊥) we have the following:
[TABLE]
Also h∘β=(C1,C2) where C1={x∈X:h(x)∈B1} and C2={x∈X:h(x)∈B2}. Similarly f∘β=(D1,D2) where D1={x∈X:f(x)∈B1} and D2={x∈X:f(x)∈B2}. Let g∘β=(E1,E2) where E1={x∈X:g(x)∈B1} and E2={x∈X:g(x)∈B2}. Thus \alpha\llbracket f\circ\beta,g\circ\beta\rrbracket=\big{(}(A_{1},A_{2})\wedge(D_{1},D_{2})\big{)}\vee\big{(}\neg(A_{1},A_{2})\wedge(E_{1},E_{2})\big{)}.
This evaluates to
[TABLE]
We show that (C1,C2)=(S1,S2) by standard set theoretic arguments.
First we prove that C1⊆S1. Let x∈C1. Then h(x)∈B1. Consider the following cases:
Case I: x∈A1: Then h(x)=f(x)∈B1 hence x∈D1. Therefore x∈A1∩D1 and so x∈S1.
Case II: x∈A2: Then h(x)=g(x)∈B1 hence x∈E1. Hence x∈A2∩E1⊆A2 we have x∈S1.
Case III: x∈/(A1∪A2): Then h(x)=⊥∈/B1 a contradiction to our assumption that h(x)∈B1. It follows that this case cannot occur.
We show that S1⊆C1. Let x∈S1. Thus x∈A1∩D1 or x\in\big{(}(A_{2}\cup(A_{1}\cap D_{2}))\cap(A_{2}\cap E_{1})\big{)}. If x∈A1∩D1 then h(x)=f(x) as x∈A1 and f(x)∈B1 as x∈D1. Thus h(x)∈B1 and so x∈C1. If x\in\big{(}(A_{2}\cup(A_{1}\cap D_{2}))\cap(A_{2}\cap E_{1})\big{)}, then x∈(A2∩E1). Thus h(x)=g(x) as x∈A2 and g(x)∈B1 as x∈E1. Hence h(x)∈B1, thus x∈C1.
We show that C2⊆S2. Let x∈C2 hence h(x)∈B2. Consider the following cases:
Case I: x∈A1: Then h(x)=f(x)∈B2, therefore x∈D2. Hence x∈A1∩D2⊆A1 and so x∈S2.
Case II: x∈A2: Then h(x)=g(x)∈B2 therefore x∈E2. Thus x∈A2∩E2⊆A2 and so x∈S2.
Case III: x∈/(A1∪A2): Then h(x)=⊥∈/B2 which is a contradiction. It follows that this case cannot occur.
Finally we show that S2⊆C2. Since A1∩A2=∅ it follows that x∈A1∩D2 or x∈A2∩E2. If x∈A1∩D2 then h(x)=f(x)∈B2 and hence x∈C2. If x∈A2∩E2 then h(x)=g(x)∈B2 hence x∈C2.
Thus α[f,g]∘β=α[[f∘β,g∘β]].
A.2. Verification of Example 2.3
Let f,g,h∈S⊥X and α,β∈3X.
Axiom (37): It is easy to see that (ζ⊥∘α)(x)=U for all x∈X.
Axiom (38): It is clear that (f∘U)(x)=U.
Axiom (39): Since S⊥ is non-trivial we must have 1=⊥. If not then for a∈S⊥∖{⊥} we have a=a⋅1=a⋅⊥=⊥ a contradiction. It follows that ζ1=ζ⊥. Hence (ζ1∘α)(x)=α(x) as ζ1(x)=1=⊥.
Axiom (40): We have
[TABLE]
Thus f∘(¬α)=¬(f∘α).
Axiom (41): We have
[TABLE]
Thus f∘(α∧β)=(f∘α)∧(f∘β).
Axiom (42): Since S⊥ has no zero-divisors we have f(x)⋅g(x)=⊥⇔f(x)=⊥ or g(x)=⊥. Consequently
[TABLE]
Thus (f⋅g)∘α=f∘(g∘α).
Axiom (43): We have
[TABLE]
Thus α[f,g]⋅h=α[f⋅h,g⋅h].
Axiom (44): Consider
[TABLE]
On the other hand
[TABLE]
Note that if h(x)=⊥ then h⋅α[f,g](x)=⊥=(h∘α)[h⋅f,h⋅g](x). Suppose that h(x)=⊥ then (h∘α)(x)=α(x). It is clear that in this case as well h⋅α[f,g](x)=(h∘α)[h⋅f,h⋅g](x) holds. Thus h⋅α[f,g]=(h∘α)[h⋅f,h⋅g].
Axiom (45): Consider
[TABLE]
We have (α[[f∘β,g∘β]])(x)=(α(x)∧(f∘β)(x))∨(¬α(x)∧(g∘β)(x)).
If f(x)=⊥ and α(x)=T we have (α[[f∘β,g∘β]])(x)=(T∧β(x))∨(F∧(g∘β)(x))=β(x)∨F=β(x)=(α[f,g]∘β)(x).
If g(x)=⊥ and α(x)=F we have (α[[f∘β,g∘β]])(x)=(F∧(f∘β)(x))∨(T∧β(x))=F∨β(x)=β(x)=(α[f,g]∘β)(x).
In all other cases it can be easily ascertained that (α[[f∘β,g∘β]])(x)=U=(α[f,g]∘β)(x). Thus α[f,g]∘β=α[[f∘β,g∘β]].
A.3. Verification of Example 2.4
Axiom (37): It is clear that ⊥∘α=U.
Axiom (38): It is obvious that t∘U=U.
Axiom (39): Since S⊥ is non-trivial it follows that 1=⊥. Consequently 1∘α=α.
Axiom (40): If s=⊥ then s∘(¬α)=U=¬(s∘α). If s=⊥ then s∘(¬α)=¬α=¬(s∘α). Thus s∘(¬α)=¬(s∘α).
Axiom (41): If s=⊥ then s∘(α∧β)=U and (s∘α)∧(s∘β)=U∧U=U. If s=⊥ then s∘(α∧β)=α∧β=(s∘α)∧(s∘β). Thus s∘(α∧β)=(s∘α)∧(s∘β).
Axiom (42): Consider s,t∈S⊥ such that s⋅t=⊥. Then (s⋅t)∘α=⊥∘α=U. Since S⊥ has no non-zero zero-divisors we have s=⊥ or t=⊥ and so s∘(t∘α)=U in either case. If s⋅t=⊥ then (s⋅t)∘α=α and s∘(t∘α)=t∘α=α as neither s nor t are ⊥. Thus (s⋅t)∘α=s∘(t∘α).
Axiom (43): As α∈{T,F,U} we consider the following three cases:
Case I: α=T: Then α[s,t]⋅u=T[s,t]⋅u=s⋅u=T[s⋅u,t⋅u].
Case II: α=F: Then α[s,t]⋅u=F[s,t]⋅u=t⋅u=F[s⋅u,t⋅u].
Case III: α=U: Then α[s,t]⋅u=U[s,t]⋅u=⊥⋅u=⊥=U[s⋅u,t⋅u].
Thus α[s,t]⋅u=α[s⋅u,t⋅u].
Axiom (44): Consider the following cases:
Case I: r=⊥: Then r⋅α[s,t]=⊥⋅α[s,t]=⊥=U[r⋅s,r⋅t]=(⊥∘α)[r⋅s,r⋅t]=(r∘α)[r⋅s,r⋅t].
Case II: r=⊥: We again consider the following three cases:
Case i: α=T: r⋅α[s,t]=r⋅T[s,t]=r⋅s=T[r⋅s,r⋅t]=(r∘T)[r⋅s,r⋅t]=(r∘α)[r⋅s,r⋅t].
Case ii: α=F: r⋅α[s,t]=r⋅F[s,t]=r⋅t=F[r⋅s,r⋅t]=(r∘F)[r⋅s,r⋅t]=(r∘α)[r⋅s,r⋅t].
Case iii: α=U: r⋅α[s,t]=r⋅U[s,t]=r⋅⊥=⊥=U[r⋅s,r⋅t]=(r∘U)[r⋅s,r⋅t]=(r∘α)[r⋅s,r⋅t].
Thus r⋅α[s,t]=(r∘α)[r⋅s,r⋅t].
Axiom (45): Consider the following three cases:
Case I: α=T: α[s,t]∘β=T[s,t]∘β=s∘β=T[[s∘β,t∘β]].
Case II: α=F: α[s,t]∘β=F[s,t]∘β=t∘β=F[[s∘β,t∘β]].
Case III: α=U: α[s,t]∘β=U[s,t]∘β=⊥∘β=U=U[[s∘β,t∘β]].
Thus α[s,t]∘β=α[[s∘β,t∘β]].
