I. predicates and sets (7.1) ------------------------------------------ ASCII NOTATION In the following, we write ``S'' for a type (\Sigma) ``s'' for an element of S (\sigma) ``P(S)'' for predicate space over S ``\in'' for set membership _ ``\meet'' for meet (| |), ``\intersect'' for intersection, ``\join'' for join (|_|), ``\union'' for union, ``\subseteq'' for non-strict subset (predicate implication), ``\supseteq'' for nonstrict superset (predicate consequence) ``\bot'' for bottom element of lattice, ``\top'' for top element of lattice, ------------------------------------------ A. predicates and sets (7.1) ------------------------------------------ PREDICATES Def: Let S be a type. Then ^ P(S) = S -> Bool is the space of *predicates* over S. PREDICATE-SET ISOMORPHISM Def: Let p: P(S) be a predicate. Then the *subset of S determined by p* is ^ A_p = { s \in S | p.s <==> T }. Def: let A \subset S be a set. Then the *characteristic predicate* for A is ------------------------------------------ How should P(S) be ordered? 1. ordering and operations on predicates ------------------------------------------ PREDICATE ORDERING Def: Let p, q: P(S). Then ^ p \subseteq Q = Corollary 7.1. (P(S),\subseteq) is a complete Boolean and atomic lattice. ------------------------------------------ Why does this corollary hold? ------------------------------------------ OPERATIONS ON PREDICATES For all s: S, p, q: P(S), define false.s == F (\bot of predicates) true.s == T (\top of predicates) (p \intersect q).s (\meet of predicates) == p.s /\ q.s (p \union q).s (\join of predicates) == p.s \/ q.s (!p).s == !(p.s) (! of predicates) (p ==> q).s (==> of predicates) == p.s ==> q.s (p <==> q).s (<==> of predicates) == (p.s <==> q.s) ------------------------------------------ What's the relation between \subseteq and ==> on predicates? What's the lattice ordering on predicates? What's the relation between == and <==> on predicates? 2. sets as predicates ------------------------------------------ CORRESPONDENCE characteristic | corresponding predicates | sets =====================|=================== p_A \subseteq p_A | A \subset B | {} true | p_A \intersect p_B | | A \union B !(p_A) | | { s: S | t } | s \in A ------------------------------------------ 3. properties of predicates B. images and indexed sets 1. images and preimages ------------------------------------------ IMAGES AND PREIMAGES Def. Let f: S -> G. Let A \subseteq S. Then the *image of A under f* is ^ im.f.A = (image) {y: G | (\exists x : x \in A : y = f.x)} Overloaded notation: write f.A for im.f.A. Def. Let f: S -> G. Then the *range of f* is ^ ran.f = f.S (range) Def. Let f: S -> G. Let B \subseteq G. Then the *preimage of f* is ^ preim.f.B = { x | f.x \in B } (preimage) -1 Notation: write f .B for preim.f.B ------------------------------------------ Is im.f : P(S) -> P(G) monotonic? strict? a join homomorphism? Is preim.f : P(G) -> P(S) monotonic? strict? a join homomorphism? 2. indexed sets ------------------------------------------ INDEXED SETS Def. Let a: S -> G and I \subset S, and let t be a term of type G. Then ^ { t | i \in I } = im.(\i . t).I Example, Let a.0 = Nat a.i = Nat -> a.(i-1) for i > 0 Then { a.i | i \in Nat } == im.a.Nat ------------------------------------------ II. inference rules for complete lattices (7.3) are the Booleans a complete lattice? The predicates? A. general meet and join ------------------------------------------ ASCII NOTATION ``<='' means the partial order (latex's \sqsubseteq) ``>='' means the reverse partial order (latex's \sqsupseteq) ``\bot'' means the least element ``\bot'' means greatest element ``==>'' means logical implication ``(\glb i \in I :: t.i)'' means meet (greatest lower bound) over the set { t.i | i \in I } ``(\lub i \in I :: t.i)'' means join (least upper bound) over the set { t.i | i \in I } ^ (\glb i \in I : b.i : t.i) = (\glb i \in { i \in I | b.i} :: t.i) ^ (\lub i \in I : b.i : t.i) = (\lub i \in { i \in I | b.i} :: t.i) ------------------------------------------ What do these mean for the booleans? 1. inference rules ------------------------------------------ INFERENCE RULES general \meet introduction: Phi, i \in I |- s <= t _________________________________ Phi |- s <= (\glb i \in I :: t) * i not free in s, Phi, or I general \meet elimination: _____________________________________ t' \in I |- (\glb i \in I :: t) <= t[i:= t'] * t' is free for i in t general \join introduction: _______________________________________ t' \in I |- t[i:= t'] <= (\lub i \in I :: t) * t' is free for i in t general \join elimination: Phi, i \in I |- t <= s _________________________________ Phi |- (\lub i \in I :: t) <= s * i not free in s, Phi, or I ------------------------------------------ What do these mean? Why the side conditions? How can you get rid of the assumptions that t' \in I in the middle two rules? Is alpha conversion valid for these? Can you formulate introduction and elimination rules for the bounded forms of the index meet and join? 2. index range homomorphisms ------------------------------------------ INDEX RANGE HOMOMORPHISMS Motivation: (\glb i \in I :: a.i) == { notation } \glb { a.i | i \in I } == { definition of image } \glb (im.a.I) == { beta conversion } (\ I . \glb (im.a.I)).I So as for fixed a: S -> G, where and G is a complete lattice (\glb i \in I :: a.i) is the following function (of I): (\ I . \glb (im.a.I)) ------------------------------------------ ------------------------------------------ HOMOMORPHISM PROPERTIES Range monotonicity: I \subseteq J ==> (\glb i \in I :: a.i) >= (\glb i \in J :: a.i) I \subseteq J ==> (\lub i \in I :: a.i) <= (\lub i \in J :: a.i) Empty range: (\glb i \in {} :: a.i) == \top (\lub i \in {} :: a.i) == \bot Range split rules: (\glb i \in (I \union J) :: a.i) == (\glb i \in I :: a.i) \meet (\glb i \in J :: a.i) (\lub i \in (I \union J) :: a.i) == (\lub i \in I :: a.i) \join (\lub i \in J :: a.i) ------------------------------------------ What do these mean for the booleans? 3. index function homomorphisms ------------------------------------------ INDEX FUNCTION HOMOMORPHISMS Suppose we fix the index set I. If a: S -> G, then (\ I . \glb (im.a.I)) : (S -> G) -> G Image monotonicity: a \sqsubseteq b ==> (\glb i \in I :: a.i) <= (\glb i \in I :: b.i) a \sqsubseteq b ==> (\lub i \in I :: a.i) <= (\lub i \in I :: b.i) Bottom and top homomorphic: i != {} ==> (\glb i \in I :: \bot.i) == \bot (\lub i \in I :: \bot.i) == \bot (\glb i \in I :: \top.i) == \top i != {} ==> (\lub i \in I :: \top.i) == \top Meet and join homomorphic: (\glb i \in I :: (a \meet b).i) == (\glb i \in I :: a.i) \meet (\glb i \in I :: b.i) (\lub i \in I :: (a \join b).i) == (\lub i \in I :: a.i) \join (\lub i \in I :: b.i) ------------------------------------------ What is \bot in S -> G? What is \top in S -> G? is indexed meet universally meet homomorphic? B. bounded quantification (7.4) ------------------------------------------ BOUNDED QUANTIFICATION NOTATION ^ (\forall i \in I :: t) = (\forall i : i \in I : t) ^ (\exists i \in I :: t) = (\exists i : i \in I : t) Thus, (\forall i \in I : b : t) == (\forall i :: i \in I /\ b ==> t) ------------------------------------------ ------------------------------------------ BOUNDED QUANTIFICATION AS INDEXED MEET AND JOIN (\forall i \in I :: t) == (/\ i \in I :: t) (\exists i \in I :: t) == (\/ i \in I :: t) So what are the rules for... Range monotonicity: I \subseteq J ==> ((\forall i \in I :: a.i) (\forall i \in J :: a.i)) I \subseteq J ==> ((\exists i \in I :: a.i) (\exists i \in J :: a.i)) Empty range: (\forall i \in {} :: a.i) == (\exists i \in {} :: a.i) == Range split rules: (\forall i \in (I \union J) :: a.i) == (\forall i \in I :: a.i) (\forall i \in J :: a.i) (\exists i \in (I \union J) :: a.i) == (\exists i \in I :: a.i) (\exists i \in J :: a.i) ------------------------------------------ 1. general conjunction and disjunction for predicates ------------------------------------------ GENERAL CONJUNCTION AND DISJUNCTION FOR PREDICATES General conjunction: (\intersect i \in I :: p.i).s <==> (\forall i \in I :: p.i.s) General disjunction: (\union i \in I :: p.i).s <==> (\exists i \in I :: p.i.s) ------------------------------------------ What inference rules would we have for these? III. selection and individuals (7.5) A. selection ------------------------------------------ SELECTION (AXIOM OF CHOICE) A new constant, the selection operator \choose : (S -> Bool) -> S Notation: (\choose v :: t) == \choose.(\ v . t) INFERENCE RULES \choose introduction: ____________________________________ Phi |- (\exists v :: t) ==> t[v := (\choose v :: t)] * if (choose v :: t) is free for v in t \choose elimination: Phi |- t ==> s _____________________________________ Phi |- t[v := (\choose v :: t)] ==> s * if v is not free in Phi or s, and if (choose v :: t) is free for v in t ------------------------------------------ ------------------------------------------ ARBITRARY ELEMENT CONSTANT For any type S ^ arb = (\choose x :: x \in S) ------------------------------------------ B. type of individuals ------------------------------------------ TYPE OF INDIVIDUALS Ind, a type with infinitely many elements infinity axiom: |- (\exists f \in Ind -> Ind :: oneone.f /\ !(onto.f)) Pictorial example: infinite finite set set . . . . . . 3 --> 4 3 2 --> 3 2 --> 3 1 --> 2 1 --> 2 0 --> 1 0 --> 1 0 0 definitions: ^ oneone.f = (\forall x x' :: f.x == f.x' ==> x == x') ^ onto.f = (\forall y :: (\exists x :: y == f.x)) ^ bijective.f = oneone.f /\ onto.f ------------------------------------------