boole.txt 0.5.6 UTF-8 dh:2024-01-15 *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* The Miser Project ================= INTERPRETATION OF BOOLEAN ALGEBRAS IN ‹ob› ------------------------------------------ Boolean Algebras have rich application in connection with digital computation [Knuth2011]. They are a treasure of insights in the organization of data representations and computations concerning them. For oMiser, enough Boolean Algebra theory is presented to illuminate important representation, interpretation and manifestation features of mathematical structures in each other and in ‹ob›. Effectively-computable representations of Boolean Algebra structures when interpreted in ‹ob› will lead to representation-preserving computational interpretations in the unfolding ‹obap› model of computation. CONTENT 1. MATHEMATICAL STRUCTURES Abstract theories of Boolean Algebras in the manner of obtheory although at a different level of abstraction 1.1 Notation and Basic Operations 1.2 Basic Constraints (Axioms) 1.3 Additional Characteristics 1.4 Interpretations 2. ‹bp› REPRESENTATIONS 2.1 Prototypical (Standard) Representation 2.2 Notable Qualities 2.3 ‹bp› Interpretation in ‹ob› 2.4 Domain-Restriction Consequences 2.5 Domain-Relaxation Equivalence 3. ‹ba› REPRESENTATIONS 3.1 Concrete Representation, ‹bn› 3.2 Boolean-Vector Structures, ‹bvn› 3.3 Concrete Interpretation: ‹bvn› - ‹bn› isomorphism 3.4 ‹ba› Simulation in ‹ob›: All-‹bvn› Interpretation ob.bvx 3.5 Circling back: Distinguishing ob.bvx as ‹ba› interpretation 4. NOTES AND REFERENCES Sources of further details and theoretical work concerning Boolean Algebras and computational matters 1. MATHEMATICAL STRUCTURES Two mathematical structures are introduced in the same manner as for ‹ob›. ‹ba› = 〈Ba,Baf,Bat〉 ‹bp› = 〈Bp,Bpf,Bpt〉 The logical theories Bpt and Bat are applications of First Order Logic with = (FOL=) using the notation introduced in Section 1 of obtheory.txt, . 1.1 Notation and Basic Operations The ‹ba› domain of discourse, Ba, is a finite set having at least two distinct members, two of which are distinguished as ⊤ and ⊥, respectively. The ‹bp› domain of discourse, Bp, consists of only the two distinguished entities and is taken as the prototypical (standard) Boolean Algebra. ⊤ (nickname "top") ⊥ (nickname "bot") The basic operations consist of a small number of functions typically expressed as operations. ~ x "comp" x, signifies the complement of x, comp(x) x ∩ y x "cap" y also known as the meet of x and y, meet(x,y) x ∪ y x "cup" y also known as the join of x and y, join(x,y) x ∸ y x "sep" y, sep(x,y) is x ∪ y excluding x ∩ y, also known as the symmetric difference, that which is separate between x and y, if anything. In addition to equality, there is also an ordering relation, x ⊆ y x "sub" y, sub(x, y) comparable to the subset relation among sets. To simplify expressions and reduce parentheses, the above listing is taken as an order of precedence, from strongest to weakest. That is x ∩ ~ y ∪ ~ x ∩ y = (x ∩ (~ y)) ∪ ((~ x) ∩ y) 1.2 Basic Constraints (Axioms) The basic conditions on all ‹ba› structures are presented in terms of axioms, arrangements that hold whatever the domain of discourse, Ba, happens to be and however the operations are defined in satisfaction of these constraints without any inconsistency. The conditions Ba1-Ba5 are standard axioms for Boolean Algebras. They are invariants, applying without exception in the context of a structure that satisfies Boolean Algebra conditions. This can also be said to constitute a Boolean Algebra interpretation of a satisfying structure. Ba1. Commutativity x ∪ y = y ∪ x x ∩ y = y ∩ x Ba2. Identity x ∪ ⊥ = x x ∩ ⊤ = x Ba3. Distributivity x ∪ (y ∩ z) = (x ∪ y) ∩ (x ∪ z) x ∩ (y ∪ z) = (x ∩ y) ∪ (x ∩ z) Ba4. Complements x ∪ ~ x = ⊤ x ∩ ~ x = ⊥ Ba5. Subordination x ⊆ y ⇔ x = x ∩ y 1.3 Additional Characteristics The following are consequences of the chosen axioms. They apply to any Boolean Algebra structure ‹ba› with distinguished domain of discourse Ba and definite basic operations satisfying Ba1-Ba5. Ba6. Associativity x ∪ (y ∪ z) = (x ∪ y) ∪ z x ∩ (y ∩ z) = (x ∩ y) ∩ z Ba7. Absorption x ∪ (x ∩ y) = x x ∩ (x ∪ y) = x Ba8. Unique Complement Pairs x = ~ ~ x x ≠ ~ x Ba9. Separation (definition) x ∸ y = x ∩ ~ y ∪ ~ x ∩ y Ba10. Partial Ordering ⊥ ⊆ y (hence "bot") x ⊆ ⊤ (hence "top") Ba11. Identity x = y ⇔ x ⊆ y ∧ y ⊆ x Ba12. The number of members in the domain of discourse Ba is even and a power of 2. 1.4 Interpretations The structures, ‹ba› and the special case ‹bp› are highly abstract. The only requirement for representing any ‹ba› is to distinguish the (finitely) enumerable members of the domain of discourse in some manner; then represent basic operations (1.1) satisfying the basic constraints (1.2). The straighforward ‹bp› flavor is known to be extremely valuable for work in logic and in computation (section 2). A related Boolean Algebra structure, ‹bvn›, is one means of interpreting all other Boolean Algebras, ‹ba›, with finite domains of discourse. ‹bvn›, along with ‹bp›, offers a means of computational interpretation of ‹ba› structures that has widespread computational application (section 3). For the Miser Project, one exploitation of the effective computability of ‹ba› structures is by establishing an interpretation in ‹ob› and then relying on the corresponding effective computability of such ‹ob› representations. That brings us to the vicinity of computational interpretation in the ‹ob› model of computation. For representations and interpretations in any domains, we'll use the functional notations (comp(x), meet(x,y), join(x,y), sub, etc.) with a naming practice that distinguishes the structure involved. Expression operators ~, ∪, ∩, etc., are only used where the intended structure is implicit or unimportant to distinguish. 2. ‹bp› REPRESENTATIONS 2.1 Standard Representation Given definite Bp = {⊥, ⊤}, in structure ‹bp› = 〈Bp,Bpf,Bpt〉, the axioms for any ‹ba› are fully satisfied by the functions represented here as bp.comp, bp.meet, bp.join, etc. bp.comp(⊥) = ⊤ bp.comp(⊤) = ⊥ bp.meet(⊤, x) = x bp.meet(⊥, x) = ⊥ bp.join(⊤, x) = ⊤ bp.join(⊥, x) = x bp.sep(⊤, x) = bp.comp(x) bp.sep(⊥, x) = x bp.sub(⊤, ⊤) bp.sub(⊥, x) 2.2 Notable Qualities * Verification of a computational interpretation of (1.3) Ba1-Ba11 by exhaustive testing is feasible in the case of ‹bp› = 〈Bp,Bpf,Bpt〉. * All effectively-computable functions, bp.f(x1, x2, ..., xn) in Bpf are representable via Bpt using only bp.comp, bp.meet, and bp.join operations along with ‹bp› equality. * Propositions of the form bp.f(x1, x2, ..., xn) = ⊤ correspond to propositional logic assertions s(p1, p2, ..., pn) by rewriting the Bt expression of bp.f such that ~ x becomes ¬ p, x ∩ y becomes p ∧ q, x ∪ y becomes p ∨ q, and x ∸ y becomes ¬ (p ⇔ q), the latter also known as exclusive-or. * The form bp.f(x1, x2, .., xn) is satisfiable if there is an assignment of {⊥, ⊤} values to individual xi such that bp.f(x1, x2, .., xn) = ⊤. The determination of satisfiability from an expression for bp.f can grow exponentially in the worst case as the number of variables increases. Whether the worst case cannot be improved figures in an important conjecture (P ≠ NP) concerning computational complexity. 2.3 ‹bp› Interpretation in ‹ob› A straightforward interpretation of ‹bp› in ‹ob› is by choosing any two distinct obs as ⊥ and ⊤ and matching the standard representation of the ‹bp› functions with functions having corresponding representations in ‹ob›. ‹bp› notion (in Bpt) an ‹ob› interpretation (in Ot) ⊥ ob.NE.bp.bot = ob.NIL ⊤ ob.NE.bp.top = ob.e(ob.NIL) bp.comp(x) ob.NE.bp.comp(x) bp.meet(x, y) ob.NE.bp.meet(x, y) bp.join(x, y) ob.NE.bp.join(x, y) bp.sep(x, y) ob.NE.bp.sep(x, y) bp.sub(x, y) ob.NE.bp.is-sub(x, y) x = y x = y supposing identification of sequence NE = [ob.NIL, ob.e(ob.NIL)] with the corresponding sequence [⊥, ⊤]. Representation of the given ‹ob› interpretation can be accomplished directly. Simply rewrite the unique representation (2.1) in Ot such that each occurrence of "bp" in the formulation is written "ob.NE.bp". Validity of the interpretation is direct. The elaborate namings, such as ob.NE.comp, reflect interpretation based on the pair NE = [ob.NIL, ob.e(ob.NIL)], distinguishing among the extensive number of distinct interpretations of ‹bp› in ‹ob›. 2.4 Domain-Restriction Consequences Whereas the ‹bp› domain of discourse has exactly two mathematical entities, that is not the case for ‹ob›. Carrying over the Bpt function representations of ‹bp› functions to corresponding representations in ‹ob› leads to partial functions in Of, ones undefined/ill-defined when an operand is neither an interpretation of ⊥ nor of ⊤. That is no such difficulty as long as operands are confined to the interpretations. The undefined cases confound computational interpretations where direct lack of definition interferes with reasoning about computations. Lack of specification also raises questions about what operational behavior must be introduced in the case of computational-interpretation infractions. 2.5 Domain-Relaxation Equivalence Alternatively, consider ob.p01.bp.comp(x), ..., ob.p01.bp.sub(x, y) with these representations: ob.p01.bp.bot = ob.NIL ob.p01.bp.top = ob.e(ob.NIL) ob.is-individual(x) ⇒ ob.p01.bp.comp(x) = ob.p01.bp.top ¬ ob.is-individual(x) ⇒ ob.p01.bp.comp(x) = ob.p01.bp.bot ob.is-individual(x) ⇒ ob.p01.bp.meet(x, y) = x ¬ ob.is-individual(x) ⇒ ob.p01.bp.meet(x, y) = y ob.is-individual(x) ⇒ ob.p01.bp.join(x, y) = y ¬ ob.is-individual(x) ⇒ ob.p01.bp.join(x, y) = x ob.is-individual(x) ⇒ ob.p01.bp.sep(x, y) = y ¬ ob.is-individual(x) ⇒ ob.p01.bp.sep(x, y) = ob.p01.bp.comp(y) ob.is-individual(x) ⇒ ob.p01.bp.sub(x, y) ¬ ob.is-individual(x) ⇒ ( ob.p01.bp.sub(x, y) ⇔ ¬ ob.is-individual(y) ) Under restriction of all operands to members of NE, the previous interpre- tation (2.3) is satisfied under domain restriction, just as in (2.4). The use of p01 is a concession to the practice of designating ‹bp› ⊥ and ⊤ with symbols 0 and 1, respectively, although the ob.p01.bp interpretation is rather different. That will be useful in interpretations of ‹ba› (section 3). This relaxed ‹ob› representation has the interesting quality that any individual is an interpretation of ⊥ and any non-individual is an interpretation of ⊤. In this case we can consider ob.NIL to be the canonical form for interpretation of ⊥ and ob.e(ob.NIL) can serve as the canonical form for interpretation of ⊤. The canonical form of an ob, x, in this interpretation is uniquelly determined by ob.p01.bp.cf(x) = ob.p01.bp.comp(ob.p01.bp.comp( x )). We can now remove the domain restriction by simply replacing the ‹ob› interpretation of x = y in (2.3) with ob.p01.bp.is-eq(x, y) ob.p01.bp.is-eq(x,y) ⇔ ob.p01.bp.comp(x) = ob.p01.bp.comp(y). because ob.p01.bp.comp only yields canonical forms and if the complements are equal so are the canonical forms. This alternative effectively partitions the obs into two equivalence classes, one of all individuals and the other of everything else, and it is the classes that are interpreted as ⊥ and ⊤, respectively. Generalizations that preserve constraints while simplifying the formulation can be seen as a form of mathematical engineering. Such approaches arise in the generalization of computational interpretations where the simplicity is important for understanding of validity and may also improve/simplify operational performance. After [Forster2003], an interpretation where "="s correspond is termed an implementation. When "="s do not correspond directly, but there is a corresponding representation in the interpretation, the interpretation is known as a simulation, the case of ob.p01.bp here. 3. ‹ba› REPRESENTATIONS When the ‹ba› = 〈Ba,Baf,Bat〉 domain of discourse, Ba, consists of more than two distinct members, finding a representation is not immediately obvious, in contrast with the handy representation of ‹bp› (section 2.1). ‹ba› representation depends on identification of the members of domain Ba and representing comp, join, and meet in Bat such that the axioms are consistently satisfied (section 1.2). The mathematical theory of Boolean Algebras provides an assurance that every Boolean Algebra is isomorphic to what is known as a concrete Boolean Algebra [Wikipedia2018a]. By isomorphic is meant, here, that interpretation of one in the other works in both directions, without domain restriction. Having representations of concrete Boolean Algebras achieves ready availability of computational interpretations for those and also whatever isomorphic ‹ba› representations are identified. 3.1 Concrete Representation, ‹bn› We define ‹bn› = 〈Bn,Bnf,Bnt〉, with natural number n > 0, to be a concrete ‹ba› structure as follows. The number of distinguished members in the domain of discourse, Bn, is even and a power of two, symbolized 2^n. Choose a set of n distinct entities, An = {a1 ,a2, ..., an}. Let Bn consist of all of the subsets of the set An, inclusive. The empty subset corresponds to ⊥; the full (sub)set corresponds to ⊤. The operations of comp, meet, and join are then represented by the set- theoretical domain-relative difference, set intersection, and set union, respectively. For example, if n = 1, A1 = {a1} then B1 has 2 members: { } (the empty set) and {a1} the entire set. Taking ⊥ = { } and ⊤ = A1, ‹b1› is isomorphic to ‹bp›. When n = 2 and A2 = {a1, a2}, B2 has 4 elements: ⊥ = { }, {a1}, {a2}, {a1, a2} = ⊤ Corresponding set-theoretic representations apply as n increases. For any ‹ba› where Ba has 2^n members, there must be a correspondence between those members and the members of Bn in structure ‹bn› such that however comp, meet, and join are represented in that ‹ba›, those functions corresponding to the comp, meet, and join of ‹bn›. This is an interpretation in ‹bn› and there will be an appropriate interpretation of the ‹ba› equality as well, providing an implementation or a simulation as the case may be. Establishment of isomorphism between a ‹ba› and a ‹bn› constitutes an interpretation of the ‹ba› in ‹bn›, and vice versa. A computational interpretation of one is, thereby, a computational interpretation of the other. It is profitable to focus on concrete representations for this purpose. 3.2 Boolean-Vector Structures, ‹bvn› The structure ‹bvn› = 〈Bvn,Bvnf,Bvnt〉, with n a natural number is a Boolean Algebra with representation as follows. The domain, Bvn, consists of all sequences [v1, v2, ..., vn], n > 0, known as n-tuples, where each vi is a member of the structure ‹bp› = 〈Bp,Bpf,Bpt〉 domain Bp. By convention, we record each vi as 0 for ⊥ and as 1 for ⊤. The Boolean Algebra representation of ‹bvn› is accomplished as follows. ⊥ identifies [0, 0, ..., 0], with n places, in Bvn ⊤ identifies [1, 1, ..., 1] similarly [x1, x2, ..., xn] = [y1, y2, ..., yn] ⇔ x1=y1 ∧ x2 = y2 ∧ ... ∧ xn = yn bvn.comp([x1, x2, ..., xn]) = [bp.comp(x1), bp.comp(x2), ..., bp.comp(xn)] bvn.join([x1, x2, ..., xn], [y1, y2, ..., yn]) = [bp.join(x1, y1), bp.join(x2, y2), ... bp.join(xn,yn)] bvn.meet([x1, x2, ..., xn], [y1, y2, ..., yn]) = [bp.meet(x1, y1), bp.meet(x2, y2), ... bp.meet(xn,yn)] bvn.sep([x1, x2, ..., xn], [y1, y2, ..., yn]) = [bp.sep(x1, y1), bp.sep(x2, y2), ... bp.sep(xn,yn)] bvn.sub(X, Y) ⇔ X = bvn.meet(X, Y) Here, each occurrence of "=" is based on the structure in which the operands are distinguished. The use of 0 and 1 disambiguates the distinction of ⊥ and ⊤ with respect to the two structures, ‹bvn› and ‹bp›. In this representation, we have presumed the ability to pair corresponding elements of ordered sequences (n-tuples) with the same number of elements. For interpretation in ‹ob›, there will be additional rigor in that accomplishment. 3.3 Concrete Interpretation: ‹bvn› - ‹bn› isomorphism ‹bvn›, thus represented (3.2), satisfies the necessary constraints (1.2) for constituting a Boolean Algebra. It is not a concrete Boolean Algebra insofar as there is no connection with subsets of sets. Isomorphism of every ‹bvn› with a concrete Boolean Algebra structure, ‹bn›, is simple and useful. For any distinguished set, An = {a1, a2, ..., an}, n > 0, establish the sequence of those distinct elements, [an, ..., a2, a1]. Correspond each entity, Xj = [xjn, ..., xj2, xj1], in the ‹bvn› domain, Bvn, with a subset in the ‹bn› domain Bn as follows. * If xji = 1, then element ai is in the Xj-corresponding subset. * If xji = 0, then element ai is not in the Xj-corresponding subset. The ‹bvn› representations (3.2) are immediately interpreted in ‹bn› with entities of the same names and with correspondence of the ‹bvn› and ‹bn› "=". The situation can be visualized in a tabulation. an a(n-1) ... a2 a1 An 0 0 ... 0 0 X0 = ⊥ 0 0 ... 0 1 X1 0 0 ... 1 0 X2 0 0 ... 1 1 X3 ... xjn xj(n-1) ... xj2 xj1 Xj ... 1 1 ... 0 0 X(2^n-4) 1 1 ... 0 1 X(2^n-3) 1 1 ... 1 0 X(2^n-2) 1 1 ... 1 1 X(2^n-1) = ⊤ All 2^n Xj are tabulated in the above scheme. The elements, Xj of domain Bvn are strictly ordered alphabetically assuming 0 before 1. The Xj are enumerated in that sequence, starting from j = 0. Each column beneath an ai in the table represents an indicator function for the associated ai, specifying 1 where ai is in that Xj row's corresponding concrete-interpretation subset and specifying 0 when that is not the case. * We can signify the indicator functions in form bvn.Iai(Xj). Note that bvn.Iai(Xj) = 1 for exactly half of the Xj. * The assertion bvn.Iai(X) = 1 is equivalent to the set-theoretical form ai ∊ X in the restricted case of An = {a1, a2, ..., an} subsets. Writing the xi values in decreasing order left-to-right is convenient for enumerating the Xj by interpreting the Xj sequence as the number j in binary notation. The result is a strict enumeration of the 2^n unique Xj. 3.4 ‹ba› Simulation in ‹ob›: Interpretation of any ‹bvn› in ob.bvx By virtue of the isomorphism between any ‹ba› and some ‹bn› (section 3.1) and thence some ‹bvn› (section 3.2), it is sufficient to interpret the ‹bvn› in ‹ob›. * For 0 and 1 vi entities in ‹bvn› n-tuples [v1, v2, ..., vn], use the interpretation ob.p01.bp in the equivalence form (section 2.5), signified I(vi). * Interpret the sequence [v1, v2, ..., vn] with the construction ob.c(I(v1), (ob.c(I(v2), ob.c(..., ob.c(I(v(n-1)), xn)...)))) where xn is restricted to a singleton under interpretation ob.p01.bp. This ‹ob› representation is abbreviated [I(v1), I(v2), ..., I(vn):] with I(vn) not a pair. * For representation of corresponding ‹bvn› and the concrete-isomorph sequence [xn, ... x2, x1] (section 3.3), interpret via ‹ob› sequence representation [I(x1), I(x2), ..., I(xn):]. Interpretation of the ‹bvn›-represented basic operations (section 1.1) is by corresponding ob.bvx functions represented as follows. ob.bvx.bot = ob.p01.bp.bot (i.e., representing [0, 0, ...] here) ob.bvx.top = ob.p01.bp.top (i.e., representing [1, 1, ...] here) ob.is-singleton(x) ⇒ ob.bvx.comp(x) = ob.p01.bp.comp(x) ¬ ob.is-singleton(x) ⇒ ob.bvx.comp(x) = ob.c( ob.p01.bp.comp(ob.a(x)), ob.bvx.comp(ob.b(x)) ) ob.is-singleton(x) ∧ ob.is-singleton(y) ⇒ ob.bvx.meet(x, y) = ob.p01.bp.meet(x, y) ob.is-singleton(x) ∧ ¬ ob.is-singleton(y) ⇒ ob.bvx.meet(x, y) = ob.bvx.meet(y, x) ¬ ob.is-singleton(x) ∧ ob.is-individual(y) ⇒ ob.bvx.meet(x, y) = y ¬ ob.is-singleton(x) ∧ ob.is-enclosure(y) ⇒ ob.bvx.meet(x, y) = x ¬ ob.is-singleton(x) ∧ ¬ ob.is-singleton(y) ⇒ ob.bvx.meet(x, y) = ob.c( ob.p01.bp.meet(ob.a(x), ob.a(y)), ob.bvx.meet(ob.b(x),ob.b(y)) ) Using the above representation of ob.bvx.meet, represent each of ob.bvx.join and ob.bvx.sep by substitution of "join" for "meet" and substitution of "sep" for "meet", respectively. Adjust the two ¬ ob.is-singleton(x) ∧ ob.is-singleton(y) cases appropriately (in the manner of section 2.1 standard operations) taking y as if one of ob.bvx.bot or ob.bvx.top. ob.is-singleton(x) ∧ ob.is-singleton(y) ⇒ ( ob.bvx.sub(x, y) ⇔ ob.p01.bp.sub(x, y) ) ob.is-individual(x) ∧ ¬ ob.is-singleton(y) ⇒ ob.bvx.sub(x, y) ob.is-enclosure(x) ∧ ¬ ob.is-singleton(y) ⇒ ( ob.bvx.sub(x, y) ⇔ ob.bvx.sub(x, ob.b(y)) ) ¬ ob.is-singleton(x) ∧ ob.is-singleton(y) ⇒ ( ob.bvx.sub(x, y) ⇔ ob.p01.bp.sub(ob.a(x), y) ∧ ob.bvx.sub(ob.b(x), y) ) ¬ ob.is-singleton(x) ∧ ¬ ob.is-singleton(y) ⇒ ( ob.bvx.sub(x, y) ⇔ ob.p01.bp.sub(ob.a(x), ob.a(y)) ∧ ob.bvx.sub(ob.b(x),ob.b(y)) ) ob.bvx.is-eq(x, y) ⇔ ob.bvx.sub(x,y) ∧ ob.bvx.sub(y,x) with the interpretation of ‹bvn› x = y being ob.bvx.is-eq(I(x),I(y)). Note some features of this interpretation. * The ob.bvx representations are total. Every ob has interpretation as a sequence under this simulation of ‹bvn› and the representation is defined over all definite obs. * Provided that the represented operations are confined to operand obs that are interpretations of ‹bvn› = 〈Bvn,Bvnf,Bvnt〉 domain elements, there is complete fidelity of ob.bvx as a simulation of ‹bvn›. * The interpretation of ‹bv1› in ob.bvx is equivalent to simulation in ob.p01.bp restricted to singletons. * When an operand sequence [x1, x2, ..., xm:] is of length less than that of another operand [y1, y2, ..., yn:], the ob.bvx representation is as if the shorter sequence is extended to match the length of the longer one by suffixing its xm element enought times, [x1, x2, ..., xm, xm, ..., xm:] * ob.bvx simulates a Boolean Algebra, one that accomodates all ‹bvn› of arbitrary (but finite) n. * Another interpretation of ob.bvx is as a simulation of binary numerals of arbitrary length. In this case, xi corresponds to 2^(i-1) and a subset corresponds to to the sum of those powers for which xi = 1. The extension of shorter sequences can be taken as viewing the shortened one as contraction of an arbitrary x. We can go farther and derive canonical forms by contraction. ob.is-singleton(x) ⇒ ob.bvx.cf(x) = ob.p01.bp.cf(x) ¬ ob.is-singleton(x) ⇒ ob.bvx.cf(x) = contraction(ob.p01.bp.cf(ob.a(x)), ob.b(x)) where ob.is-singleton(y) ⇒ contraction(x, y) = trimback(x, ob.p01.bp.cf(y)) ¬ ob.is-singleton(y) ⇒ contraction(x, y) = contraction(ob.c(ob.p01.bp.cf(ob.a(y)),x), ob.b(y)) where ob.is-singleton(x) ∧ x = y ⇒ trimback(x, y) = y ob.is-singleton(x) ∧ x ≠ y ⇒ trimback(x, y) = ob.c(x, y) ¬ ob.is-singleton(x) ∧ ob.a(x) = y ⇒ trimback(x, y) = trimback(ob.b(x), y) ¬ ob.is-singleton(x) ∧ ob.a(x) ≠ y ⇒ trimback(x, y) = repack(x, y) where ob.is-singleton(x) ⇒ repack(x, y) = ob.c(x, y) ¬ ob.is-singleton(x) ⇒ repack(x, y) = repack(ob.b(x), ob.c(ob.a(x), y)) Here the auxiliary function representations for contraction, trimback, and repack are internal to the representation of ob.bvx.cf(x). There are preconditions only satisfied by how the subordinate representations are appealed to in the representation of their superiors, above. These together ensure that the result is an ob.bvx canonical form. ob.bvx.cf(x) is an ob sequence in which the elements are ob.p01.bp.cf canonical forms, whether labelled as ⊥ and ⊤ or 0 and 1. Furthermore, ob.bvx.cf(x) is the shortest ob sequence, [v1:] or [v1, v2, ..., v(n-1), vn:], where v(n-1) is different than vn. It can be seen that [0:] in this notation is equivalent to [0, 0, 0, ...], hence the ⊥ of ‹bvx›, and [1:] is equivalent to [1, 1, 1, ...] and hence the ⊤. 3.5 Circling back: Distinguishing ob.bvx as ‹ba› interpretation Concluding that the representation, ob.bvx, is amenable to interpretation of any Boolean Algebra in ‹ob› leaves open questions about which Boolean Algebra and which interpretation thereof, and how is that conveyed. Assuming some sequence, An = [a1, a2, ..., an], the indicator functions (section 3.3), can be represented as follows. Associate, with An, the corresponding vectors Vn = [[1,0:], [0,1,0:], ..., [0,...,0,1:]] where the last has n-1 leading 0's and V1 = [[1:]]. Then ob.bvx.sub(vi, x) ⇔ ob.bvx.bvn.Iai(x) = 1, by definition. In order to interpret a specific ‹bvn›, n > 0, in ob.bvx, one can clamp the canonical forms such that only n bits of variation are in the interpretation and the set of canonical forms. ob.bvx.bvn.top = [1,...,1,0:] "with n 1's" ob.bvx.bvn.clamp(x) = ob.bvx.meet(x, ob.bvx.bvn.top) ob.bvx.bvn.cf(x) = ob.bvx.comp(ob.bvx.comp(ob.bvx.bvn.clamp(x) ) ). That some ob.bvx vectors have an additional (n+1)-th position does not impact taking other ob.bvx operations as ob.bvx.bvn operations, provided that the ‹bvn› x = y is interpreted in ‹ob› as ob.bvx.bvn.cf(x) = ob.bvx.bvn.cf(y) and ob.bvx.bvn.sub(x,y) ⇔ ob.bvx.sub(ob.bvx.bvn.clamp(x), y) Association with ai is still implicit and also order-dependent. It is tempting to go farther and present the association explicitly, say with Mn = [[v1, I(a1)], [v2, I(a2)], ..., [vn, I(an)]] where we require some manner of interpretation/expression of the ai, internal to the structure, especially in simple domains such as that of ‹ob›. For interpretation in ‹ob› by means such as ob.bvx, there are two important circumstances to be dealt with, especially when carried into computational-interpretation: the designation of the ai and preserving association with vi in operands of the represented primitive operations. Such implementation/simulation exigencies apply in the reduction to computation no matter the simplicity of the mathematical formulations. There are provisions in computational systems that bring some order to securing of interpretation constraints by computational means, including reconciliation between what appear to be incompatible interpretations of the same structures. Investigation of those prospects is left to consideration of extensions to the basic ‹ob› model of computation. 4. NOTES AND REFERENCES Do not regard the elaborate formulations, especially for interpretations in ‹ob›, as a liability of mathematical formulations and reliance on logical deductions. Rather, the elaborate cases are a consequence of having to encode (represent as data) entities in mathematical domains using only the primitive notions of ‹ob›. In so doing, we retain the opportunity to reason about the representations using mathematical methods such as structural induction. And, wherever an interpretation is valid, it is often helpful to reason in the structure being interpreted rather than in the structure having the interpretation. It should be clear, from this treatment of Boolean Algebra interpretation, that there is no basis for determining what an intended interpretation is simply by inspection of an ob. One can ascertain whether an ob admits of being a particular interpretation, and sometimes the contrary. Yet there is no intrinsic means by which any ob is confined to some unique, self- evident interpretation no matter the tacit appeal. This fluidity of interpretation and its usage in ob.bvx slides into a computational commonplace that is easy to overlook. In the formulation of ‹bvn›, there is explicit reliance on ‹bp› which remains abstract in that arrangement. Interpretation via ob.bvx.bvn (and general ob.bvx) has fixed interpretation of ‹bp›, namely ob.p01.bp. That is exploited in somewhat-simplified ob.bvx representations that are streamlined based on known features of ob.p01.bp. This coupling becomes inflexible compared with an approach that, for example, makes ob....bp representations substitutable via some formulation such as ob.bvx(ob...bp), maintaining harmony with reliance on abstract ‹bp› in structure ‹bvn›. The prospect of interpretation composition modularizes the validation of computational interpretations, a capability worth investigation. Software developers will recognize this pattern in the use of templates in some object- oriented programming systems. A primeval counterpart at the level of the ‹ob› computational model will be investigated. The extension of an interpretation to representation via equivalence classes is an appealing idiom for computational interpretations. The specific relaxation in (2.5) is reminiscent of provision in LISP, with atom NIL taken as ⊥, and in C-inspired languages, with 0 taken as ⊥. Anything else is taken as ⊤. Canonical forms, however, are revealed by the results of relational operators, such as x ≠ y, in those programming systems. Limitation of ‹ba› to a finite domain of discourse having at least two members is appropriate for computational interpretations and oMiser. Although there are Boolean Algebras having unbounded domains, that is not considered here, even though formulation of ob.bvx is suggestive of a denumerable, exponentially-growing case including representation of 2's-complement binary arithmetic. Formulation of ‹ba› is an amalgam of the Boolean Algebra treatments cited below. Symbols ⊤ and ⊥ are chosen to restrain the common use of 1 and 0. Assumption that 0 and 1 signify numbers and also binary bits is avoided here, although 0 and 1 are notationally convenient for ‹bvn› and have historical roots in [Boole1834] and practical application to binary representations in digital computation [Knuth2011]. Explicit interpre- tions of arithmetics in ‹ob› extends beyond Boolean Algebra. Symbols for Boolean operations are kept distinct from the logical connectives used in FOL= notation, hence the use of complement, meet, join, sep symbols and fussiness in qualifying names of function representations by the name of the particular structure and interpreta- tion, if any. These notational devices facilitate recognition of correspondences without implying identity, avoiding for a time any tacit collapsing of separate notions together as if about the same theoretical entities. * Miser Project: Representing Functions in ‹ob›'s Abstract World. Orcmid's Live Hideout blog article, available at in a series of posts that articulate ‹ob› structure, featuring representations include those for Boolean Algebra, here. This material prefaces introduction of the model of computation, * Hamilton, Dennis E. ‹ob› Mathematical Structure. 2018-11-17 article obtheory.txt 0.2.1, accessed on the Internet at . The mathematical formulation of the essential structure. [Boole1854] Boole, George. An Investigation of the Laws of Thought: on which are founded the mathematical theories of logic and probabilities. Dover (New York: 1958), original 1854 edition reprinted with all corrections made within the text. ISBN 0-486-60028-9 [EncycMath2012] Boolean algebra. 2012-04-04 article accessed on the Internet at . [Forster2003] Forster, Thomas. Reasoning About Theoretical Entities. World Scientific (New Jersey: 2003). ISBN 981-238-567-3 [Knuth2011] Knuth, Donald E. Zeros and Ones. Section 7.1, pp. 47-280 in The Art of Computer Programming, Volume 4A: Combinatorial Algorithms, Part 1. Addison-Wesley (Upper Saddle River, NJ: 2011). ISBN 978-0-201-03804-0 [Rosenbloom1950] Rosenbloom, Paul C. The Logic of Classes. Chapter 1, pp. 1-27 in The Elements of Mathematical Logic. Dover (New York: 1950). ISBN 0-486-60227-3 pbk. [Stoll1979] Stoll, Robert R. Boolean Algebra. Chapter 6, pp. 248-288 in Set Theory and Logic. Dover (New York: 1979). ISBN 0-486-63829-4 [Wikipedia2018a] Boolean algebra. 2018-11-04 article accessed on the Internet at . [Wikipedia2018b] Boolean algebra (structure). 2018-11-06 article accessed on the Internet at . *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* Copyright 2018-2024 Dennis E. Hamilton Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at http://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* ATTRIBUTION Hamilton, Dennis E. Interpretation of Boolean Algebras in ‹ob›. Miser Theory Conception text file boole.txt version 0.5.6 dated 2024-01-15, available on the Internet as a version of *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* TODO: * Reflect all of the citations made here in orcmid.github.io/bib/ * When representation, interpretation, manifestation, implementation, and simulation are worked out more clearly, review these materials for consistent usage and links to related resources of the project and and elsewhere, especially ones of reference/historical value. * Find an accessible reference to the conclusion of representation of non- concrete ‹ba›s via isomorphisms to concrete ‹ba›s. Stone's theorem may be too much of a stretch. * Address ob.bvx being an optimization of the composition of of one representation in another, exploiting structural characteristics of obs. The result is interpretation-preserving. The route is from an interpre- tation ob.p01.bp of ‹bp› into an interpretation ob.bvx.ba that involves composition with ob.p01.bp in a manner that preserves the constituent interpretation. In computational-system terms, there is primeval presence of the idea of templates and certain ideas of classes and types. * Since we are now sort-of following obap/, there is also the prospect of creating scripts and using an applicative function to shorten the cases that can be handled by a mapa kind of function (in honor of mapcar). * The use of all the dots in names here needs to be rethought, since the use of "." in term names doesn't quite work. There is also an "using" situation here. I am unclear how that works in oFrugal 1.0, but it is worth pondering. *---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--* 0.5.6 2024-01-15T21:15Z Adust title, small touch-ups 0.5.5 2023-11-10T19:47Z Refactoring staged to orcmid.github.io/miser/obrep/ 0.5.4 2023-11-10T19:31Z Creation of tombstone as part of refactoring to docs/ 0.5.3 2022-08-01T20:17Z Touch-Ups 0.5.2 2019-03-06-11:31 Raise the prospect of primeval representation compositions. Manage TODOs. Some touch-ups 0.5.1 2019-01-10-10:48 Touch-ups 0.5.0 2019-01-01-15:43 Clean up 2.5, with corrected sub(x,y) and simpler is-eq(x,y) 0.4.2 2018-12-17-10:50 Correct title of Section 3.4 0.4.1 2018-12-12-12:44 Cleanup Section 3.6 interpretation ob.bvx.bvn. 0.4.0 2018-12-12-11:14 Touch-ups and streamlining of 3.4 ob.bvx to short- circuit operations with different-length operands where possible. 0.3.1 2018-12-11-15:00 Add bvx clamping to fixed n as an option in 3.5. 0.3.0 2018-12-10-13:20 Tuning, Manage TODOs, cross-reference, and simplify ob.bvx significantly. 0.2.0 2018-12-07-15:25 Review and smooth as needed for the post on "Representing Functions in ‹ob›’s Abstract World", also putting more care in offering of ob.bvx with addition of section 3.5. 0.1.2 2018-12-03-10:19 touch-ups to section 2.3 wording for accuracy. 0.1.1 2018-12-03-09:34 touch-ups for smoother Live Hideout blog quotation. 0.1.0 2018-12-01-11:49 More corrections, adjustment of notation, some smoothing declaration ready for prime-time as 0.1.0. 0.0.11 2018-11-30-14:19 Correct some typos and a howler about = now correct at BA11 in section 1.3. 0.0.10 2018-11-28-14:53 Complete sections 3.4-3.5 and wrap up the essential draft of coverage for oMiser purposes. 0.0.9 2018-11-26-14:32 Smooth some and complete section 3.4 giving one ‹ba› interpretation in ‹ob›. 0.0.8 2018-11-25-10:31 Complete the bvn interpretation in bn. Repair text flow and rework 3.3. 0.0.7 2018-11-24-12:41 Expand ‹ba› representation to interpretation of Boolean-Vector Boolean Algebras in concrete Boolean algebras that can then represent any Boolean Algebra on a finite and distinguished domain of discourse. 0.0.6 2018-11-22-12:12 More smoothing and addition of 3.1 on concrete ‹ba› representations. 0.0.5 2018-11-21-11:10 Proofing corrections, text improvements, and revamping of section 2 to bring out the interpretation considerations more fully. 0.0.4 2018-11-20-14:55 Manage TODOs. Complete section 2. Wordsmith. 0.0.3 2018-11-19-11:49 Refine in preparation for ‹bp› Interpretation in ‹ob›. 0.0.2 2018-11-18-12:14 Expand and refine coverage to ‹bp› representation. 0.0.1 2018-11-15-14:38 Manage TODOs. Replace ⨁ with ∸ for symmetric difference. Draft essentials of structures ‹ba› and ‹bp›. Add initial references. 0.0.0 2018-11-13-10:38 Placeholder and boiler plate for bridging between Boolean Algebras and computational interpretations in ‹ob›. *** end of boole.txt ***