2 Problem Definition

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-nameexpr]...))
(define/x-instanceid([field-nameexpr]...))
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-verifierinst-argcert-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.1Core Datatype🔗 i

procedure
( equal? ab)→boolean
a:any
b:any

Test if a and b are equal.

2.1.1Atomic Type🔗 i

type-descriptor
( 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.

type-descriptor
boolean

type-descriptor
symbol

2.1.2Set🔗 i

type-descriptor / procedure
( set maybe-element-typemaybe-size)
(set e...)

maybe-element-type =
| #:of-typeelement-type

maybe-size =
| #:sizesize

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

type-descriptor
( subset-of supersetmaybe-size)

maybe-size =
| #:sizenatural-number
| #:sizevalue-descriptor

superset : value-descriptor?Set?

type-descriptor
( element-of a-set)

a-set : value-descriptor?Set?

value-descriptor
( the-set-of a-type)

a-type : type-descriptor?

This value descriptor gives the abstract set consisting of all elements of given type.

procedure
( set-∈ eS)→boolean?
e:any
S:set?

Test if e is in set S.

procedure
( set-∉ eS)→boolean?
e:any
S:set?

Test if e is NOT in set S.

procedure
( set-size S)→natural?
S:set?

Get the size (cardinality) of set S, i.e., |S| where S is S

procedure
( set-∩ S...+)→set?
S:set?

Get the intersection of the sets S ... .

procedure
( set-∪ S...+)→set?
S:set?

Get the intersection of two sets S ... .

procedure
( set-minus S1S2)→set?
S1:set?
S2:set?

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.

syntax
( ∀ [x∈X]pred-x)

X : set?
pred-x : boolean-expression?

Universial quantifier expression over set X. Test if all element x in X satisfy pred-x.

syntax
( ∃ [x∈X]pred-x)

X : set?
pred-x : boolean-expression?

Existential quantifier expression over set X. Test if there exists some element x of X satisfies pred-x.

syntax
( ∃<=1 [x∈X]pred-x)

X : set?
pred-x : boolean-expression?

Test if at most 1 element x in X satisfies pred-x.

syntax
( ∃=1 [x∈X]pred-x)

X : set?
pred-x : boolean-expression?

Test if exactly 1 element x in X satisfies pred-x.

syntax
( sum val-xfor[x∈X]maybe-condition)

maybe-condition =
| ifpred-x

X : set?
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).

syntax
( max val-xfor[x∈X]maybe-condition)

maybe-condition =
| ifpred-x

X : set?
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).

syntax
( min val-xfor[x∈X]maybe-condition)

maybe-condition =
| ifpred-x

X : set?
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.3Tuple🔗 i

type-descriptor
( tuple field-type...+)

field-type = #:field-typetype

type : type-descriptor?

A tuple is a (ordered) sequence with fixed length.

value-descriptor
( product-ofa-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.

procedure
( tpl e...+)→tuple?
e:any

Create a tuple with components e ... .

NOT available in verifier definitions

procedure
( fst t)→any
t:tuple?

Get the first component of tuple t.

procedure
( snd t)→any
t:tuple?

Get the second component of tuple t.

procedure
( trd t)→any
t:tuple?

Get the third component of tuple t.

procedure
( frh t)→any
t:tuple?

Get the forth component of tuple t.

procedure
( ffh t)→any
t:tuple?

Get the fifth component of tuple t.

procedure
( n-th tn)→any
t:tuple?
n:natural?

Get the n-th component of tuple t.

top ← prev up next →