AmateurB

Embedding formal methods in Clojure since 2016.

Functions

Functions are special relations, that map an element from its domain to at most one element of its range.

Sets of Functions

lisb=> (+-> #{1 2} #{4 3})   ;; B: {1, 2}+->{4, 3}
#{#{[1 -> 4] [2 -> 4]} #{[1 -> 4] [2 -> 3]} #{[1 -> 3] [2 -> 4]} #{} #{[2 -> 3] [1 -> 3]} #{[2 -> 4]} #{[2 -> 3]} #{[1 -> 3]} #{[1 -> 4]}}
lisb=> (partial-function #{1 2} #{4 3})   ;; B: {1, 2}+->{4, 3}
#{#{[1 -> 4] [2 -> 3]} #{} #{[1 -> 4]} #{[2 -> 3]} #{[1 -> 3]} #{[2 -> 4]} #{[2 -> 3] [1 -> 3]} #{[1 -> 3] [2 -> 4]} #{[2 -> 4] [1 -> 4]}}

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

lisb=> (+->> #{1 2} #{4 3})   ;; B: {1, 2}+->>{4, 3}
#{#{[2 -> 3] [1 -> 4]} #{[1 -> 3] [2 -> 4]}}
lisb=> (partial-surjection #{1 2} #{4 3})   ;; B: {1, 2}+->>{4, 3}
#{#{[2 -> 3] [1 -> 4]} #{[2 -> 4] [1 -> 3]}}

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

lisb=> (>+> #{1 2} #{4 3})   ;; B: {1, 2}>+>{4, 3}
#{#{} #{[1 -> 3]} #{[2 -> 4] [1 -> 3]} #{[2 -> 3] [1 -> 4]} #{[2 -> 4]} #{[1 -> 4]} #{[2 -> 3]}}
lisb=> (partial-injection #{1 2} #{4 3})   ;; B: {1, 2}>+>{4, 3}
#{#{[2 -> 3] [1 -> 4]} #{[1 -> 3]} #{} #{[2 -> 3]} #{[2 -> 4] [1 -> 3]} #{[2 -> 4]} #{[1 -> 4]}}

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

lisb=> (>+>> #{1 2} #{4 3})   ;; B: {1, 2}>+>>{4, 3}
#{#{[2 -> 4] [1 -> 3]} #{[1 -> 4] [2 -> 3]}}
lisb=> (partial-bijection #{1 2} #{4 3})   ;; B: {1, 2}>+>>{4, 3}
#{#{[2 -> 3] [1 -> 4]} #{[2 -> 4] [1 -> 3]}}

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

Lambda Expression

lisb=> (lambda [:x] (member? :x #{1 2}) (inc :x))   ;; B: %(x).(x:{1, 2}|succ(x))
#{[1 -> 2] [2 -> 3]}

Function Call

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

Note that the association of the maplets is important:

lisb=> (fn-call #{(|-> 1 (|-> 2 3))} 1 2)   ;; B: {(1, (2, 3))}(1, 2)
lol, broken