2 Problem Definition

8.17.0.6

2 Problem Definition🔗ℹ

package: Karp

syntax
is-a

Can only be used inside decision-problem.

syntax
(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🔗ℹ

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

Test if a and b are equal.

2.1.1 Atomic Type🔗ℹ

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.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

type-descriptor
(subset-of superset maybe-size)

maybe-size =
| #:size natural-number
| #:size value-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-∈ e S) → boolean?
e : any
S : set?

Test if e is in set S.

procedure
(set-∉ e S) → 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 S1 S2) → 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-x for [x ∈ X] maybe-condition)

maybe-condition =
| if pred-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-x for [x ∈ X] maybe-condition)

maybe-condition =
| if pred-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-x for [x ∈ X] maybe-condition)

maybe-condition =
| if pred-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.3 Tuple🔗ℹ

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

field-type = #:field-type type

type : type-descriptor?

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

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

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 t n) → any
t : tuple?
n : natural?

Get the n-th component of tuple t.

1	Getting Started with Karp, by Example
2	Problem Definition
3	Reduction
4	Structure Libraries