-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathFunctions.tla
150 lines (129 loc) · 9.19 KB
/
Functions.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
------------------------------ MODULE Functions -----------------------------
(***************************************************************************)
(* `^{\large\bf \vspace{12pt} *)
(* Notions about functions including injection, surjection, and bijection.*)
(* Originally contributed by Tom Rodeheffer, MSR. *)
(* \vspace{12pt}}^' *)
(***************************************************************************)
LOCAL INSTANCE Folds
(***************************************************************************)
(* Restriction of a function to a set (should be a subset of the domain). *)
(***************************************************************************)
Restrict(f,S) == [ x \in S |-> f[x] ]
(***************************************************************************)
(* Restriction of a function to the subset of its domain satisfying a *)
(* test predicate. *)
(* *)
(* Example: *)
(* (LET f == (0 :> "a" @@ 1 :> "b" @@ 2 :> "c") *)
(* IN RestrictDomain(f, LAMBDA x : x \in {0,2})) *)
(* = (0 :> "a" @@ 2 :> "c") *)
(***************************************************************************)
RestrictDomain(f, Test(_)) == Restrict(f, {x \in DOMAIN f : Test(x)})
(***************************************************************************)
(* Restriction of a function to the subset of its domain for which the *)
(* function values satisfy a test predicate. *)
(* *)
(* Example: *)
(* (LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) *)
(* IN RestrictValues(f, LAMBDA y : y \in {0,2})) *)
(* = ("a" :> 0 @@ "b" :> 2) *)
(* *)
(* This is similar to the operator SelectSeq from the standard Sequences *)
(* module and related to standard "filter" functions in functional *)
(* programming. However, SelectSeq produces sequences, whereas *)
(* RestrictValues will in general not. For example, *)
(* *)
(* RestrictValues([0,1,2], LAMBDA y : y \in {0,2}) *)
(* = (1 :> 0 @@ 3 :> 2) *)
(***************************************************************************)
RestrictValues(f, Test(_)) ==
LET S == {x \in DOMAIN f : Test(f[x])}
IN Restrict(f, S)
(***************************************************************************)
(* Range of a function. *)
(* Note: The image of a set under function f can be defined as *)
(* Range(Restrict(f,S)). *)
(***************************************************************************)
Range(f) == { f[x] : x \in DOMAIN f }
(***************************************************************************)
(* The inverse of a function. *)
(* Example: *)
(* LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) *)
(* IN Inverse(f, DOMAIN f, Range(f)) = *)
(* (0 :> "a" @@ 1 :> "b" @@ 2 :> "c") *)
(* Example: *)
(* LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) *)
(* IN Inverse(f, DOMAIN f, {1,3}) = *)
(* 1 :> "b" @@ 3 :> "a") *)
(***************************************************************************)
Inverse(f,S,T) == [t \in T |-> CHOOSE s \in S : t \in Range(f) => f[s] = t]
(***************************************************************************)
(* The inverse of a function. *)
(***************************************************************************)
AntiFunction(f) == Inverse(f, DOMAIN f, Range(f))
(***************************************************************************)
(* A function is injective iff it maps each element in its domain to a *)
(* distinct element. *)
(* *)
(* This definition is overridden by TLC in the Java class Functions.java *)
(* The operator is overridden by the Java method with the same name. *)
(***************************************************************************)
IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b
(***************************************************************************)
(* Set of injections between two sets. *)
(***************************************************************************)
Injection(S,T) == { M \in [S -> T] : IsInjective(M) }
(***************************************************************************)
(* A map is a surjection iff for each element in the range there is some *)
(* element in the domain that maps to it. *)
(***************************************************************************)
Surjection(S,T) == { M \in [S -> T] : \A t \in T : \E s \in S : M[s] = t }
(***************************************************************************)
(* A map is a bijection iff it is both an injection and a surjection. *)
(***************************************************************************)
Bijection(S,T) == Injection(S,T) \cap Surjection(S,T)
(***************************************************************************)
(* An injection, surjection, or bijection exists if the corresponding set *)
(* is nonempty. *)
(***************************************************************************)
ExistsInjection(S,T) == Injection(S,T) # {}
ExistsSurjection(S,T) == Surjection(S,T) # {}
ExistsBijection(S,T) == Bijection(S,T) # {}
--------------------------------------------------------------------------------
FoldFunction(op(_,_), base, fun) ==
(***************************************************************************)
(* Applies the binary function op on all elements of seq in arbitrary *)
(* order starting with op(f[k], base). The resulting function is: *)
(* op(f[i],op(f[j], ..., op(f[k],base) ...)) *)
(* *)
(* op must be associative and commutative, because we can not assume a *)
(* particular ordering of i, j, and k *)
(* *)
(* Example: *)
(* FoldFunction(LAMBDA x,y: {x} \cup y, {}, <<1,2,1>>) = {1,2} *)
(***************************************************************************)
MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, DOMAIN fun)
FoldFunctionOnSet(op(_,_), base, fun, indices) ==
(***************************************************************************)
(* Applies the binary function op on the given indices of seq in arbitrary *)
(* order starting with op(f[k], base). The resulting function is: *)
(* op(f[i],op(f[j], ..., op(f[k],base) ...)) *)
(* *)
(* op must be associative and commutative, because we can not assume a *)
(* particular ordering of i, j, and k *)
(* *)
(* indices must be a subset of DOMAIN(fun) *)
(* *)
(* Example: *)
(* FoldFunctionOnSet(LAMBDA x,y: {x} \cup y, {}, <<1,2>>, {}) = {} *)
(***************************************************************************)
MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, indices)
=============================================================================
\* Modification History
\* Last modified Fri Oct 13 09:49:52 CEST 2023 by kulpreet
\* Last modified Tue Nov 01 08:46:11 CET 2022 by merz
\* Last modified Mon Apr 05 03:25:53 CEST 2021 by marty
\* Last modified Wed Jun 05 12:14:19 CEST 2013 by bhargav
\* Last modified Fri May 03 12:55:35 PDT 2013 by tomr
\* Created Thu Apr 11 10:30:48 PDT 2013 by tomr