8.16.0.2
2 Problem Definition🔗ℹ
| (decision-problem #:name name | | #:instance ([field-name is-a type-descriptor] ...+) | | #:certificate type-descriptor) |
|
Defines a decision problem name with its instance
and certificate structures.
Defining a decision problem x’s structure enables 3 other language constructs:
The constructor for x-instance:
| (create-x-instance ([field-name expr] ...)) |
| (define/x-instance id ([field-name expr] ...)) |
The order of
field-names does not need to match the order they are defined
in
decision-problem.
The field accessors for each field of an instance, which are just the field-names.
The define-x-verifier definition form to define the verifier of problem x.
| (define-x-verifier inst-arg cert-arg | | body ...+) |
|
The id of the verifier of problem x is x-verifier. It also enables the solver
function x-solver, which can be called by the user when debugging the reduction.
x-solver takes an x-instance and produce a certificate of the instance or reports
no solution.
2.1 Core Datatype🔗ℹ
Test if a and b are equal.
2.1.1 Atomic Type🔗ℹ
(natural maybe-length)
|
| |
| maybe-length | | = | | | | | | | | | #:cardinal | | | | | | | #:numeric |
|
#:cardinal specifies that the value is encoded in unary. Hence, the numeric value
of the number is polynomial to the input size.
#:numeric specifies that the value is encoded in binary.
Hence, the numeric value of the number is exponential to the the input size. To guarantee a reduction
runs in polynomial time to the input size, certain operations are not allowed on such numbers.
When not specified, #:cardinal is assumed by default.
2.1.2 Set🔗ℹ
type-descriptor / procedure (set maybe-element-type maybe-size)
|
| (set e ...) |
| |
| maybe-element-type | | = | | | | | | | | | #:of-type element-type | | | | | | | | maybe-size | | = | | | | | | | | | #:size size |
|
| |
| | element-type | | : | | type-descriptor? |
| | size | | : | | value-descriptor? Natural? |
|
type-descriptor: When maybe-element-type is not specified, there is no restriction
on the element type of the set.
procedure: create a set with elements e ... .
NOT available inside verifier definitions
(subset-of superset maybe-size)
|
| |
| maybe-size | | = | | | | | | | | | #:size natural-number | | | | | | | #:size value-descriptor |
|
| |
| | superset | | : | | value-descriptor? Set? |
|
This value descriptor gives the abstract set consisting of all elements of given type.
(set-∈ e S) → boolean?
|
| e : any |
| S : set? |
Test if e is in set S.
(set-∉ e S) → boolean?
|
| e : any |
| S : set? |
Test if e is NOT in set S.
Get the size (cardinality) of set S, i.e.,
|S| where S is S
(set-∩ S ...+) → set?
|
| S : set? |
Get the intersection of the sets S ... .
(set-∪ S ...+) → set?
|
| S : set? |
Get the intersection of two sets S ... .
Get a set consisting of all elements in S1 but not S2, i.e.
S_1 \setminus S_2 where S_1, S_2 are S1,S2 respectively.
(∀ [x ∈ X] pred-x)
|
| |
| | pred-x | | : | | boolean-expression? |
|
Universial quantifier expression over set X.
Test if all element x in X satisfy pred-x.
(∃ [x ∈ X] pred-x)
|
| |
| | pred-x | | : | | boolean-expression? |
|
Existential quantifier expression over set X.
Test if there exists some element x of X satisfies pred-x.
(∃<=1 [x ∈ X] pred-x)
|
| |
| | pred-x | | : | | boolean-expression? |
|
Test if at most 1 element x in X satisfies pred-x.
(∃=1 [x ∈ X] pred-x)
|
| |
| | pred-x | | : | | boolean-expression? |
|
Test if exactly 1 element x in X satisfies pred-x.
(sum val-x for [x ∈ X] maybe-condition)
|
| |
| maybe-condition | | = | | | | | | | | | if pred-x |
|
| |
| | val-x | | : | | interger-expression? |
| | pred-x | | : | | boolean-expression? |
|
Calculate
\sum_{x \in X , P(x)}f(x)
where the expression val-x of x is f(x)
and the expression pred-x of x is P(x).
(max val-x for [x ∈ X] maybe-condition)
|
| |
| maybe-condition | | = | | | | | | | | | if pred-x |
|
| |
| | val-x | | : | | interger-expression? |
| | pred-x | | : | | boolean-expression? |
|
Calculate
\max_{x \in X , P(x)}\{f(x)\}
where the expression val-x of x is f(x)
and the expression pred-x of x is P(x).
(min val-x for [x ∈ X] maybe-condition)
|
| |
| maybe-condition | | = | | | | | | | | | if pred-x |
|
| |
| | val-x | | : | | interger-expression? |
| | pred-x | | : | | boolean-expression? |
|
Calculate
\min_{x \in X , P(x)}\{f(x)\}
where the expression val-x of x is f(x)
and the expression pred-x of x is P(x).
2.1.3 Tuple🔗ℹ
(tuple field-type ...+)
|
| |
| field-type | | = | | #:field-type type |
|
| |
|
A tuple is a (ordered) sequence with fixed length.
(product-of a-set ...+)
|
| |
| | a-set | | : | | value-descriptor? Set? |
|
The value specified by this value descriptor is the set consisting of all tuples with
the element on each component coming from a-set ... in order.
(tpl e ...+) → tuple?
|
| e : any |
Create a tuple with components e ... .
NOT available in verifier definitions
Get the first component of tuple t.
Get the second component of tuple t.
Get the third component of tuple t.
Get the forth component of tuple t.
Get the fifth component of tuple t.
(n-th t n) → any
|
| t : tuple? |
| n : natural? |
Get the n-th component of tuple t.