8.12
3 Reduction🔗ℹ
Define a forward instance construction function from decision
problem from-name to decision problem to-name
with name id. The function takes one from-name-instance
as its arugment and produces one to-name-instance as its output.
The final expression of the body is expected to evaluate to an
to-name-instance.
Define a forward certificate construction function from decision
problem from-name to decision problem to-name
with name id. The function takes one from-name-instance
and a from-name-certificate of the instance
as its arugments and produces one to-name-certificate as its output.
The final expression of the body is expected to evaluate to an
to-name-certificate.
Define a forward certificate construction function from decision
problem from-name to decision problem to-name
with name id. The function takes one from-name-instance
and a to-name-certificate of the instance
as its arugments and produces one from-name-certificate as its output.
The final expression of the body is expected to evaluate to an
from-name-certificate.
Use target-inst to
access the to-problem instance constructed from the current from-problem instance through
the supplied forward instance construction.
Define id as the result of expr.
| (check-reduction #:from from-name #:to to-name | | maybe-from-generator maybe-n-test maybe-random-seed | | f->t-instance-construction | | f->t-certificiate-construction | | t->f-certificate-construction) |
|
| |
| maybe-from-generator | | = | | | | | | | | | #:from-generator generator | | | | | | | | maybe-n-test | | = | | | | | | | | | #:n-test n-test | | | | | | | | maybe-random-seed | | = | | | | | | | | | #:random-seed random-seed |
|
| |
|
Run random testing on the given reduction.
The f->t-instance-construction,
f->t-certificiate-construction and t->f-certificate-construction
arguments should be construction functions defined with
define-forward-instance-construction, define-forward-certificate-construction
and define-backward-certificate-construction respectively.
Access counterexample instance of the from-problem found by the last run of
check-reduction.
Import the decision problem definitions from
file-1 and
file-2.
union-in
takes care of the fields that share the same name across the two decision problems.
3.1 Additional Operations🔗ℹ
The additional operations described in this section are NOT available in verifier definitions.
(if cond-expr then-expr else-expr)
|
\begin{cases}
a & p \\
b & o.w.
\end{cases}
where a is then-expr, b is else-expr, and
p is cond-expr
(for/set { el-expr element-in-set ...+ maybe-cond})
|
| |
| element-in-set | | = | | for [var ∈ X] | | | | | | | | var | | = | | x | | | | | | | (x #:index i) | | | | | | | | maybe-cond | | = | | if cond-expr | | | | | | | |
|
| |
| | cond-expr | | : | | boolean-expression? |
|
Create a set with representative element el-expr going over all element x
in X ... satisfying the cond-expr, i.e.,
\{ f(x,y,\dots) \mid x \in X(y,\dots), y \in Y(\dots),P(x,y,\dots) \}
where f(x,y,\dots) is the value produced by el-expr.
In this example, the elements of the set are sums of a and b,
where a and b are drawn from the sets \{1,2,3\} and \{4,5,6\}, respectively.
| > (for/set {(+ a b) | | for [a ∈ (set 1 2 3)] | | for [b ∈ (set 4 5 6)]}) |
|
{5ₚ, 6ₚ, 7ₚ, 8ₚ, 9ₚ} |
When the form [(e #:index j) ∈ X] is used, j is bound to the index
of x in set X.
Example
| > (define set-of-abc (set "a" "b" "c")) |
| > (for/set {(set e1 e2 j) | | for [(e1 #:index j) ∈ set-of-abc] | | for [(e2 #:index k) ∈ set-of-abc] | | if (not (equal? j k))}) |
|
{{3ₚ, "b", "a"}, {1ₚ, "b", "c"}, {2ₚ, "c", "a"}, {1ₚ, "b", "a"}, {3ₚ, "c", "a"}, {2ₚ, "b", "c"}} |
If
x is an element of a set created with
for/set,
(corr x) produces one element that
x is created from.
(find-one [var ∈ X] maybe-cond)
|
| |
| var | | = | | x | | | | | | | (x #:index i) | | | | | | | | maybe-cond | | = | | s.t. cond-expr |
|
| |
| | cond-expr | | : | | boolean-expression? |
|
Get an (arbitary) element from set X that satisfies the condition. An error
will be triggered if no such elemenet exists.
When the form [(x #:index i) ∈ X] is used,
i is bound to the index of x in set X.
(argmax x-expr [x ∈ X] maybe-cond)
|
| |
| maybe-cond | | = | | s.t. cond-expr |
|
| |
| | x-expr | | : | | number-expression? |
| | cond-expr | | : | | boolean-expression? |
|
(argmin x-expr [x ∈ X] maybe-cond)
|
| |
| maybe-cond | | = | | s.t. cond-expr |
|
| |
| | x-expr | | : | | number-expression? |
| | cond-expr | | : | | boolean-expression? |
|
Produce a set containing all pairs (2-tuple) of elements in set X.
Produce a set containing all triplets (3-tuple) of elements in set X.
(el subscript ...) → abstract-element
|
| subscript : any |
An abstract element with subscripts subscript ... .
Get the first subscript of e ... .
Get the second subscript of e ... .
Get the third subscript of e ... .
(_ks e k) → any
|
| e : el? |
| k : positive-integer? |
Get the k-th subscript of e ... .
(index-in e S) → natural?
|
| e : any |
| S : set? |
Get the index of the e in set S.
Get the element in set S of index i.
(ints-from-to from to) → (setof natural?)
|
| from : natural? polynomial-size? |
| to : natural? polynomial-size? |
Produce the set of integers from from to to inclusive of the endpoints. The endpoints must
be within polynomial of the input size.