Project

Namespaces

Public Vars

latte-sets.powerrel

Notions about the relational powerset construction.

This is akin to latte-sets.powerset but for relations.

fetch-powerrel-types

(fetch-powerrel-types def-env ctx r-type)

powerrel

(powerrel [T :type] [U :type])
(==> (rel T U) :type)

Definition: The powerset constructor for relations.

The term (powerrel T U)' is the type of sets whose elements are relations of type(rel T U)`.

rel-elem

(rel-elem [R (rel T U)] [X (powerrel T U)])
(X R)

Definition: Membership for powersets. Th relation R is an element of the set X.

rel-ex

(rel-ex [X (powerrel T U)])
(forall [α :type] (==> (forall [R (rel T U)] (==> (rel-elem R X) α)) α))

Definition: The powerset existential for relations.

There exists an element relation R of the powerset X such that…

This is the definition of latte.quant/ex but adpated for relations.

rel-ex-elim

(rel-ex-elim [X (powerrel T U)] [A :type])
(==> (rel-ex X) (forall [R (rel T U)] (==> (rel-elem R X) A)) A)

Theorem: The elimination rule for the relation existential.

rel-ex-intro

(rel-ex-intro [X (powerrel T U)] [R (rel T U)])
(==> (rel-elem R X) (rel-ex X))

Theorem: Introduction rule for rel-ex.

rel-single

(rel-single [X (powerrel T U)])
(forall [R S (rel T U)] (==> (rel-elem R X) (rel-elem S X) (releq R S)))

Definition: The relational powerset version of latte-prelude.quant/single. There is a single relation element in X such that…

rel-unique

(rel-unique [X (powerrel T U)])
(and (rel-ex X) (rel-single X))

Definition: The relational powerset version of latte-prelude.quant/unique. There exists a unique relation R in the set of relations X such that …

rintersections

(rintersections [RR (powerrel T U)])
(lambda
 [x T]
 (lambda [y U] (forall [R (rel T U)] (==> (rel-elem R RR) (R x y)))))

Definition: Generalized relational intersection.

rintersections-lower-bound

(rintersections-lower-bound [RR (powerrel T U)])
(forall
 [R (rel T U)]
 (==> (rel-elem R RR) (subrel (rintersections RR) R)))

Theorem: The generalized intersection is a lower bound wrt. the subrel relation.

rintersections-prop

(rintersections-prop [P (==> T U :type)] [RR (powerrel T U)])
(forall
 [R (rel T U)]
 (==>
  (rel-elem R RR)
  (forall [x T] (forall [y U] (==> (R x y) (P x y))))
  (forall
   [x T]
   (forall [y U] (==> ((rintersections RR) x y) (P x y))))))

Theorem: Preservation of properties on relational intersections.

runions

(runions [RR (powerrel T U)])
(lambda
 [x T]
 (lambda
  [y U]
  (rel-ex (lambda [R (rel T U)] (and (rel-elem R RR) (R x y))))))

Definition: Generalized relation union.

runions-upper-bound

(runions-upper-bound [RR (powerrel T U)])
(forall [R (rel T U)] (==> (rel-elem R RR) (subrel R (runions RR))))

Theorem: The generalized relational union is an upper bound wrt. the subrel relation.

the-rel

(the-rel [X (powerrel T U)] [u (rel-unique X)])
(rel T U)

Axiom: The relation powerset version of latte-prelude.quant/the.

the-rel-lemma

(the-rel-lemma [X (powerrel T U)] [u (rel-unique X)])
(forall [R (rel T U)] (==> (rel-elem R X) (releq R (the-rel X u))))

Theorem: The unique relation … is unique.

the-rel-prop

(the-rel-prop [X (powerrel T U)] [u (rel-unique X)])
(rel-elem (the-rel X u) X)

Axiom: The property of the unique set descriptor the-rel.

trans-closure

(trans-closure [R (rel T T)])
(rintersections (trans-closure-set R))

Definition: The transitive closure of R, cf. rel/transitive Remark: it is defined in the powerrel namespace because the definition requires rintersections.

trans-closure-set

(trans-closure-set [R (rel T T)])
(lambda [S (rel T T)] (and (subrel R S) (transitive S)))

Definition: The set of transitively-closed relation.

trans-closure-smallest

(trans-closure-smallest [R (rel T T)])
(forall
 [S (rel T T)]
 (==> (subrel R S) (transitive S) (subrel (trans-closure R) S)))

Theorem:

trans-closure-sub

(trans-closure-sub [R (rel T T)])
(subrel R (trans-closure R))

Theorem:

transitive-trans-closure

(transitive-trans-closure [R (rel T T)])
(transitive (trans-closure R))

Theorem: