AmateurB

Embedding formal methods in Clojure since 2016.

Relations over two sets are a subset of the cartesian product of two sets. It contains only tuples with the first element in the first base set, and the second in the other.

Maplet / Tuple

lisb=> (maplet 1 2)   ;; B: (1, 2)
[1 -> 2]
lisb=> (maplet 1 "foo")   ;; B: (1, "foo")
[1 -> foo]
lisb=> (|-> 1 "foo")   ;; B: (1, "foo")
[1 -> foo]
B => 1|->2
[1 -> 2]
B => (1,2)
[1 -> 2]

Sets of Relations

The operators below describes the set of all possible relations (which are total, surjective or both total and surjective):

lisb=> (<-> #{1 2} #{4 5})   ;; B: {1, 2}<->{4, 5}
#{#{[1 -> 4] [1 -> 5] [2 -> 4]} #{[2 -> 4] [2 -> 5]} #{[1 -> 5] [2 -> 4]} #{[2 -> 5]} #{} #{[1 -> 5] [2 -> 5] [1 -> 4]} #{[1 -> 5] [2 -> 5]} #{[2 -> 4]} #{[2 -> 4] [1 -> 5] [2 -> 5]} #{[1 -> 4] [2 -> 5]} #{[1 -> 5] [1 -> 4]} #{[1 -> 4] [2 -> 4]} #{[2 -> 4] [2 -> 5] [1 -> 4]} #{[1 -> 5]} #{[2 -> 5] [1 -> 4] [1 -> 5] [2 -> 4]} #{[1 -> 4]}}
lisb=> (relation #{1 2} #{4 5})   ;; B: {1, 2}<->{4, 5}
#{#{[1 -> 5] [2 -> 4] [2 -> 5]} #{[2 -> 5] [1 -> 5]} #{[2 -> 5]} #{[1 -> 4] [2 -> 4] [1 -> 5] [2 -> 5]} #{} #{[2 -> 4] [1 -> 4]} #{[1 -> 4] [2 -> 5]} #{[2 -> 5] [1 -> 5] [1 -> 4]} #{[1 -> 5]} #{[1 -> 4] [1 -> 5]} #{[2 -> 4]} #{[2 -> 4] [1 -> 5] [1 -> 4]} #{[2 -> 5] [2 -> 4] [1 -> 4]} #{[2 -> 4] [2 -> 5]} #{[1 -> 4]} #{[2 -> 4] [1 -> 5]}}

Total Relation

lisb=> (<<-> #{1 2} #{4 5})   ;; B: {1, 2}<<->{4, 5}
#{#{[2 -> 5] [1 -> 5] [1 -> 4]} #{[2 -> 4] [1 -> 4] [2 -> 5]} #{[2 -> 5] [1 -> 5]} #{[1 -> 5] [2 -> 4] [2 -> 5] [1 -> 4]} #{[1 -> 5] [2 -> 4]} #{[1 -> 4] [2 -> 5]} #{[2 -> 4] [1 -> 4] [1 -> 5]} #{[2 -> 4] [1 -> 4]} #{[1 -> 5] [2 -> 5] [2 -> 4]}}
lisb=> (total-relation #{1 2} #{4 5})   ;; B: {1, 2}<<->{4, 5}
#{#{[2 -> 5] [1 -> 4] [2 -> 4]} #{[2 -> 5] [1 -> 5] [2 -> 4]} #{[2 -> 5] [1 -> 5]} #{[1 -> 5] [1 -> 4] [2 -> 4]} #{[2 -> 5] [1 -> 4] [1 -> 5]} #{[2 -> 4] [1 -> 5]} #{[2 -> 5] [1 -> 4]} #{[2 -> 4] [1 -> 4]} #{[1 -> 4] [2 -> 4] [2 -> 5] [1 -> 5]}}

Surjective Relation

lisb=> (<->> #{1 2} #{4 5})   ;; B: {1, 2}<->>{4, 5}
#{#{[2 -> 5] [2 -> 4]} #{[2 -> 5] [1 -> 5] [1 -> 4]} #{[1 -> 4] [2 -> 4] [1 -> 5]} #{[2 -> 4] [2 -> 5] [1 -> 4]} #{[1 -> 5] [1 -> 4]} #{[1 -> 5] [2 -> 4] [2 -> 5] [1 -> 4]} #{[2 -> 4] [2 -> 5] [1 -> 5]} #{[2 -> 5] [1 -> 4]} #{[1 -> 5] [2 -> 4]}}
lisb=> (surjective-relation #{1 2} #{4 5})   ;; B: {1, 2}<->>{4, 5}
#{#{[2 -> 5] [1 -> 4]} #{[2 -> 5] [1 -> 4] [1 -> 5]} #{[2 -> 5] [2 -> 4] [1 -> 5]} #{[2 -> 5] [2 -> 4] [1 -> 4]} #{[2 -> 4] [1 -> 4] [1 -> 5]} #{[1 -> 5] [2 -> 4]} #{[1 -> 5] [1 -> 4]} #{[2 -> 5] [2 -> 4]} #{[2 -> 4] [1 -> 4] [2 -> 5] [1 -> 5]}}

Total Surjective Relation

lisb=> (<<->> #{1 2} #{4 5})   ;; B: {1, 2}<<->>{4, 5}
#{#{[1 -> 4] [2 -> 5] [2 -> 4]} #{[1 -> 4] [2 -> 5]} #{[2 -> 4] [1 -> 5]} #{[1 -> 5] [2 -> 5] [2 -> 4]} #{[2 -> 5] [1 -> 4] [1 -> 5]} #{[2 -> 4] [1 -> 4] [2 -> 5] [1 -> 5]} #{[1 -> 5] [1 -> 4] [2 -> 4]}}
lisb=> (total-surjective-relation #{1 2} #{4 5})   ;; B: {1, 2}<<->>{4, 5}
#{#{[2 -> 4] [1 -> 5] [1 -> 4]} #{[1 -> 5] [2 -> 4]} #{[1 -> 4] [2 -> 5]} #{[1 -> 5] [2 -> 5] [1 -> 4]} #{[2 -> 5] [1 -> 5] [2 -> 4]} #{[2 -> 5] [2 -> 4] [1 -> 4]} #{[2 -> 4] [2 -> 5] [1 -> 4] [1 -> 5]}}

Domain and Range

lisb=> (dom #{(|-> 2 2) (|-> 1 3) (|-> 1 2)})   ;; B: dom({(2, 2), (1, 3), (1, 2)})
#{1 2}
lisb=> (ran #{(|-> 2 2) (|-> 1 3) (|-> 1 2)})   ;; B: ran({(2, 2), (1, 3), (1, 2)})
#{3 2}

Identity Relation

lisb=> (id #{1 3 2})   ;; B: id({1, 3, 2})
#{[1 -> 1] [3 -> 3] [2 -> 2]}

Restrictions and Subtractions

lisb=> (<| #{1} #{(|-> 2 2) (|-> 1 3) (|-> 1 2)})   ;; B: {1}<|{(2, 2), (1, 3), (1, 2)}
#{[1 -> 3] [1 -> 2]}
lisb=> (domain-restriction #{1} #{(|-> 2 2) (|-> 1 3) (|-> 1 2)})   ;; B: {1}<|{(2, 2), (1, 3), (1, 2)}
#{[1 -> 2] [1 -> 3]}
lisb=> (<<| #{1} #{(|-> 2 2) (|-> 1 3) (|-> 1 2)})   ;; B: {1}<<|{(2, 2), (1, 3), (1, 2)}
#{[2 -> 2]}
lisb=> (domain-subtraction #{1} #{(|-> 2 2) (|-> 1 3) (|-> 1 2)})   ;; B: {1}<<|{(2, 2), (1, 3), (1, 2)}
#{[2 -> 2]}
lisb=> (|> #{(|-> 2 2) (|-> 1 3) (|-> 1 2)} #{2})   ;; B: {(2, 2), (1, 3), (1, 2)}|>{2}
#{[2 -> 2] [1 -> 2]}
lisb=> (range-restriction #{(|-> 2 2) (|-> 1 3) (|-> 1 2)} #{2})   ;; B: {(2, 2), (1, 3), (1, 2)}|>{2}
#{[1 -> 2] [2 -> 2]}
lisb=> (|>> #{(|-> 2 2) (|-> 1 3) (|-> 1 2)} #{2})   ;; B: {(2, 2), (1, 3), (1, 2)}|>>{2}
#{[1 -> 3]}
lisb=> (range-subtraction #{(|-> 2 2) (|-> 1 3) (|-> 1 2)} #{2})   ;; B: {(2, 2), (1, 3), (1, 2)}|>>{2}
#{[1 -> 3]}

Inverse

lisb=> (inverse #{[2 -> 2] [1 -> 3] [1 -> 2]})   ;; B: {(2, 2), (1, 3), (1, 2)}~
#{[2 -> 2] [3 -> 1] [2 -> 1]}

Relational Image

lisb=> (image #{(|-> 3 42) (|-> 2 2) (|-> 1 3) (|-> 1 2)} #{1 2})   ;; B: {(2, 2), (1, 3), (1, 2), (3, 42)}[{1, 2}]
#{3 2}

Misc Operators

lisb=> (<+ #{(|-> 1 3) (|-> 1 2) (|-> 2 3)} #{(|-> 4 0) (|-> 1 0)})   ;; B: {(2, 3), (1, 3), (1, 2)}<+{(1, 0), (4, 0)}
#{[1 -> 0] [4 -> 0] [2 -> 3]}
lisb=> (override #{(|-> 1 3) (|-> 1 2) (|-> 2 3)} #{(|-> 4 0) (|-> 1 0)})   ;; B: {(2, 3), (1, 3), (1, 2)}<+{(1, 0), (4, 0)}
#{[2 -> 3] [4 -> 0] [1 -> 0]}
lisb=> (>< #{(|-> 3 4) (|-> 1 2) (|-> 2 3)} #{(|-> 2 6) (|-> 4 4)})   ;; B: {(2, 3), (3, 4), (1, 2)}><{(4, 4), (2, 6)}
#{[2 -> [3 -> 6]]}
lisb=> (direct-product #{(|-> 3 4) (|-> 1 2) (|-> 2 3)} #{(|-> 2 6) (|-> 4 4)})   ;; B: {(2, 3), (3, 4), (1, 2)}><{(4, 4), (2, 6)}
#{[2 -> [3 -> 6]]}
lisb=> #{(and (member? (|-> :x :y) #{(|-> 3 4) (|-> 1 2) (|-> 2 3)}) (member? (|-> :x :z) #{(|-> 2 6) (|-> 4 4)})) | [:x :y :z]}   ;; B: {x,y,z|(x, y):{(2, 3), (3, 4), (1, 2)} & (x, z):{(4, 4), (2, 6)}}
#{[2 -> 3 -> 6]}
lisb=> (composition #{(|-> 3 4) (|-> 1 2) (|-> 2 3)} #{(|-> 2 6) (|-> 4 4)})   ;; B: ({(2, 3), (3, 4), (1, 2)};{(4, 4), (2, 6)})
#{[1 -> 6] [3 -> 4]}
lisb=> #{(exists [:z] (and (member? (|-> :x :z) #{(|-> 3 4) (|-> 1 2) (|-> 2 3)}) (member? (|-> :z :y) #{(|-> 2 6) (|-> 4 4)}))) [:x :y] |}   ;; B: {x,y|#(z).((x, z):{(2, 3), (3, 4), (1, 2)} & (z, y):{(4, 4), (2, 6)})}
#{[1 -> 6] [3 -> 4]}
lisb=> (parallel-product #{(|-> 3 4) (|-> 1 2)} #{(|-> 5 6) (|-> 7 8)})   ;; B: ({(3, 4), (1, 2)}||{(7, 8), (5, 6)})
#{[1 -> 7 -> [2 -> 8]] [3 -> 5 -> [4 -> 6]] [1 -> 5 -> [2 -> 6]] [3 -> 7 -> [4 -> 8]]}
lisb=> #{[(|-> (|-> :x :v) (|-> :y :w))] (and (member? (|-> :x :y) #{(|-> 3 4) (|-> 1 2)}) (member? (|-> :y :w) #{(|-> 5 6) (|-> 7 8)})) |}   ;; B: {((x, v), (y, w))|(x, y):{(3, 4), (1, 2)} & (y, w):{(7, 8), (5, 6)}}
lol, broken

Projection

The projection functions allow extracting the first or the second element of a tuple, respectively. They must be parameterized with the correct sets.

lisb=> (prj1 nat-set nat-set)   ;; B: prj1(NAT, NAT)
#{[0 -> 3 -> 0] [1 -> 1 -> 1] [3 -> 0 -> 3] [2 -> 1 -> 2] [3 -> 3 -> 3] [2 -> 3 -> 2] [2 -> 0 -> 2] [2 -> 2 -> 2] [3 -> 2 -> 3] [0 -> 2 -> 0] [0 -> 1 -> 0] [1 -> 2 -> 1] [3 -> 1 -> 3] [0 -> 0 -> 0] [1 -> 3 -> 1] [1 -> 0 -> 1]}
lisb=> (fn-call (prj1 nat-set nat-set) (bmaplet 1 2))   ;; B: prj1(NAT, NAT)((1, 2))
1
lisb=> (fn-call (prj2 nat-set nat-set) (bmaplet 1 2))   ;; B: prj2(NAT, NAT)((1, 2))
2
lisb=> (fn-call (prj2 string-set nat-set) (bmaplet 1 2))   ;; B: prj2(STRING, NAT)((1, 2))
lol, broken

Closures

The closure operator seems to keep the set symbolic.

lisb=> (closure #{(|-> 3 4) (|-> 1 2) (|-> 2 3) (|-> 4 2)})   ;; B: closure({(2, 3), (3, 4), (4, 2), (1, 2)})
lol, broken
lisb=> (closure1 #{(|-> 3 4) (|-> 1 2) (|-> 2 3) (|-> 4 2)})   ;; B: closure1({(2, 3), (3, 4), (4, 2), (1, 2)})
#{[4 -> 2] [3 -> 4] [1 -> 3] [4 -> 4] [3 -> 3] [2 -> 2] [4 -> 3] [1 -> 2] [1 -> 4] [3 -> 2] [2 -> 4] [2 -> 3]}
lisb=> (iterate #{(|-> 3 4) (|-> 1 2) (|-> 2 3) (|-> 4 2)} 1)   ;; B: iterate({(2, 3), (3, 4), (4, 2), (1, 2)}, 1)
#{[4 -> 2] [3 -> 4] [2 -> 3] [1 -> 2]}
lisb=> (iterate #{(|-> 3 4) (|-> 1 2) (|-> 2 3) (|-> 4 2)} 2)   ;; B: iterate({(2, 3), (3, 4), (4, 2), (1, 2)}, 2)
#{[4 -> 3] [3 -> 2] [1 -> 3] [2 -> 4]}
lisb=> (iterate #{(|-> 3 4) (|-> 1 2) (|-> 2 3) (|-> 4 2)} 3)   ;; B: iterate({(2, 3), (3, 4), (4, 2), (1, 2)}, 3)
#{[3 -> 3] [1 -> 4] [4 -> 4] [2 -> 2]}

Relation to Function, Function to Relation

lisb=> (fnc #{(|-> 2 4) (|-> 1 3) (|-> 1 2)})   ;; B: fnc({(2, 4), (1, 3), (1, 2)})
#{[1 -> #{3 2}] [2 -> #{4}]}
lisb=> (rel #{(|-> 1 #{1 2}) (|-> 2 #{4})})   ;; B: rel({(2, {4}), (1, {1, 2})})
#{[1 -> 2] [2 -> 4] [1 -> 1]}