Problems as Input, Output, Certificate and Definition: SPADE structures and verifies them #32

Goal

A contributor should describe a Redux problem with four fields: Input, Output, Certificate and a free-form Definition. SPADE produces the structured text from the first three, and uses them to:

1. parse and verify problem instances;
2. parse and verify certificates (in the Verifier);
3. let solvers write their Big-O in the Input's variables, and evaluate it on a given instance from those variables' values;
4. do the same for reductions;
5. do the same through chains of reductions, by composing the Big-O functions (Big-O in a problem's input variables, evaluated per instance and composed through reductions Redux#893).

This is the format Dr. Bodily asked for (Oct 15). It replaces this issue's earlier plan to generate the problem's meaning from quantifiers and named predicates.

The format (Clique)

Input: (G, k) where

• G = (V, E) is an ordered pair (representing a graph) where
  • V is a set of values (representing vertices)
  • E is a set of unordered pairs of values (representing unweighted, undirected edges) such that E is a subset of V unorderedcross V
• k is an integer (representing a threshold) such that 0 ≤ k ≤ |V|

Output: True or False

Certificate: C is a set of values such that C is a subset of V

Definition: The Clique problem asks whether there is a subset C of V of size ≥ k such that there is an edge in E between every two vertices in C.

• Structure (the where nesting, "is an ordered pair", "a set of unordered pairs of values") comes from the SPADE grammar.
• Underlined parts are constraints SPADE verifies.
• Italic parts are descriptions the contributor writes for readers. SPADE stores them but doesn't check them.
• A value is an integer or a string.
• Everything else belongs in the free-form Definition.

What a contributor would write for this:

Input:       {(G,k) | G = (V,E), V is set of value "vertices",
              E subset V unorderedcross V "unweighted, undirected edges",
              k is int "a threshold", 0 <= k <= |V|}
Output:      True or False
Certificate: {C | C subset V}
Definition:  The Clique problem asks whether there is a subset C of V of size ≥ k
             such that there is an edge in E between every two vertices in C.

The syntax is a proposal; the sub-issues settle it.

Pieces

1. Describe a definition without parsing an instance: Describe a definition's names and types without parsing an instance #18 (PR feat(definition): describe a definition's parts without parsing an instance #24, 0.2.0).
2. Fix the checks that don't check: fix(grammar): x is <set> and undefined names check nothing #14 and (Low Priority) Basic type and size checks in the grammar #6.
3. Name nested groups: G = (V,E), Name nested groups in a definition string, e.g. G = (V,E) #37.
4. Sets of values: V is set of value, Sets and lists of plain values: V is set of value #38.
5. Cardinality and comparisons: 0 <= k <= |V|, Cardinality and comparisons in constraints: |X|, 0 <= k <= |V| #33.
6. Descriptions as annotations: V is set "vertices", Variable descriptions (representing …): annotations in the grammar or on the Redux side #36. Whether these live in SPADE or Redux is still open.
7. Certificate grammars that refer to the instance's names: C subset V, part of Grammars that can describe every certificate shape #5.
8. Mappings and value grammars: weighted edges, SAT literals, Mappings and value grammars: per-element weights and SAT literals #35.
9. Matrices and tensors: Matrices and tensors: declare n-dimensional values with shape checks #30.

Deferred: #34 (named predicates and quantifier-style conditions). The meaning of a certificate goes in the Definition and the Verifier, so SPADE doesn't need to express it.

Problems this would have caught

Writing out examples from today's hand-written Redux text turned up errors in three of four problems, and an inconsistency in the fourth:

• Vertex Cover: the Output describes the verifier ("whether the given set of nodes is a vertex cover").
• Knapsack: the Input never mentions V, though the Output uses it. The grammar names the capacity and target w and v, while the text says W and V.
• Clique: the certificate grammar {K | K is set} reuses K, which already names the threshold.
• Hamiltonian Cycle: the certificate example {1,2,4,5,3} is a set, which can't hold an order.

Related (not re-parented)

• Build problems' Input and Output text from their SPADE grammars Redux#891: build the Input/Output/Certificate text from the grammars.
• Big-O in a problem's input variables, evaluated per instance and composed through reductions Redux#893: Big-O in the Input's variables, evaluated and composed through reductions.
• Parse every certificate with SPADE, and make SPADE handle whitespace Redux#627: move Redux's verifiers to SPADE.
• Split instances into named parts from their SPADE grammar, through one instanceParts endpoint Redux#851: the instance parts editor, which reads the same definition description.