8.18
4.3 mapping
| (require karp/lib/mapping) | package: Karp |
procedure
(lookup f k) → any
f : mapping? k : nay
Get the image of k under the mapping f.
The lookup keyword can be omitted in the verifier definition,
i.e., use (f k) instead of (lookup f k).
procedure
(dom f) → any
f : mapping?
Get the domain set of the mapping f.
type-descriptor / procedure
(mapping #:from domain #:to codomain maybe-disjoint)
(mapping [k ~> v] ...)
maybe-disjoint =
| #:disjoint
domain : value-descriptor? Set?
codomain : value-descriptor? Set?
type-descriptor: #:disjoint can only be used when the codomain is a family of sets, i.e., a set of sets. It requires the images of each pair of elements being disjoint.
procedure: create a mapping with key-value pairs (k,v) ... .
NOT available inside verifier definitions
| (require karp/lib/mapping-reduction) | package: Karp |
syntax
(mapping x-in-X-to-img ...+)
x-in-X-to-img = [x ∈ X] maybe-pred-x ~> | img-expr maybe-pred-x = where pred-x
X : set?
pred-x : boolean-expression?
Create a mapping of the form
m(x) = \begin{cases} f(x) & x \in X \text{ and } P(x) \\ \dots\end{cases},
where x is X, f(x) is img-expr and P(x) is pred-x. If one elements appears multiple times in the definition, its element in the mapping is determined by the last apperance of the x-in-X-to-img sequence.
curr provides access the mapping object
that has been constructed up to the point before curr
inside the mapping constructor.