Games And Mechanisms

Grid treats a game as live model data, not as a separate simulation program. Players, strategies, payoffs, reports, priors, allocations, and tree nodes may come from cells, Frames, Graph projections, or Predicate-backed relations. Editing any dependency invalidates the ordinary LIR call that consumes it.

All strategic conclusions carry an honesty status and replayable evidence. Finite checks either examine the complete declared domain within their budget or return an error; they never publish a partial search as a proof.

Declarative games

A finite normal-form game is most naturally defined from three relations:

Players = ["row"; "column"]
 
Strategies = [
  "row", "cooperate";
  "row", "defect";
  "column", "cooperate";
  "column", "defect"
]
 
# Strategy columns follow Players; payoff columns follow in the same order.
Payoffs = [
  "cooperate", "cooperate", 3, 3;
  "cooperate", "defect",    0, 5;
  "defect",    "cooperate", 5, 0;
  "defect",    "defect",    1, 1
]
 
game PrisonersDilemma {
  players = Players
  strategies = Strategies
  payoffs = Payoffs
}

The block lowers to the ordinary named assignment PrisonersDilemma = GAME.NORMAL_FORM(Players, Strategies, Payoffs). It adds no new evaluator or wire format. Player and strategy order defines stable numeric profile indexes; duplicate names, missing profiles, unknown strategies, and non-finite payoffs fail validation.

An extensive-form game uses an explicit typed tree object:

game EntryGame {
  extensive = TreeSpecification
}
 
SubgamePerfect = GAME.EXTENSIVE(EntryGame)

This form lowers through GAME.EXTENSIVE_FORM. The current certified lane is finite perfect information, including chance nodes. Every non-root node must have exactly one parent. Cycles, shared nodes, unreachable nodes, implicit information sets, invalid probabilities, and exhausted node budgets fail closed. GAME.EXTENSIVE returns child-before-parent values and every local choice comparison needed to replay the backward-induction certificate.

Imperfect information is explicit rather than inferred from shared nodes:

game HiddenAction {
  imperfect = InformationSetTree
}
 
Equilibrium = GAME.IMPERFECT(HiddenAction)

Every decision node names an informationSet. Nodes in one set must belong to the same player, expose the same ordered actions, and preserve that player's own remembered information-set/action history. The current certified lane is finite, two-player, zero-sum, and perfect recall. It performs an exact bounded reduction to pure contingent plans, reuses the independent maximin/minimax certificate, and returns both mixed plans and realization-equivalent behavior at each information set. Plan, profile, and tree-evaluation limits fail closed without publishing a partial equilibrium.

Compact graphical games retain local payoff scopes directly:

game LocalInteraction { graphical = LocalPayoffFactors }
Equilibria = GAME.GRAPHICAL(LocalInteraction)

GAME.GRAPHICAL_FORM validates one complete local factor per player without constructing the global payoff product. GAME.GRAPHICAL uses the interaction graph for min-fill ordering and partial-assignment pruning, then returns every pure Nash profile with replayable local best-response certificates. The resident Graph-handle path uses the same contract while additionally caching disconnected strategic components by semantic fingerprint.

Analysis and verification

GAME.ANALYZE(game, options?) exhaustively returns:

• pure Nash equilibria and profitable-deviation counterexamples;
• per-profile and global regret;
• weak and strict dominant strategies;
• the Pareto frontier; and
• social-welfare maximizers.

GAME.VERIFY(game, claim, options?) gives a uniform passed, status, witness envelope suitable for a cell, Predicate publication, or WHY trace. Claims use tagged objects such as:

IsEquilibrium = GAME.VERIFY(
  PrisonersDilemma,
  {property: "pure_nash", profile: [1, 1]}
)
 
LowRegret = GAME.VERIFY(
  PrisonersDilemma,
  {property: "regret_at_most", profile: [1, 1], bound: 0}
)

Supported properties are has_pure_nash, pure_nash, pareto_efficient, regret_at_most, and dominant_strategy.

Certified equilibrium lanes

Use the narrowest solver that matches the claim:

Solver-backed results are certified_approximate under the authored epsilon. The support-enumeration budget is deliberately visible through maxDeviations, since candidate supports grow exponentially. GAME.NASH refuses when that complete bounded search cannot be attempted. Correlated equilibria accept "feasibility" or "welfare" as the optional objective.

Cooperative, matching, and congestion games

Specialized declarative forms retain their domain structure instead of forcing an exponentially larger payoff table:

game Consortium { cooperative = CharacteristicFunction }
game Residency { matching = PreferenceMarket }
game Traffic { congestion = RouteGame }
 
Shares = GAME.COOPERATIVE(Consortium)
Placement = GAME.STABLE_MATCH(Residency)
Routes = GAME.CONGESTION(Traffic)

GAME.COOPERATIVE requires the complete finite characteristic function, computes exact Shapley values, and checks efficiency plus every coalition constraint for Shapley core membership. GAME.STABLE_MATCH accepts strict, possibly incomplete preference lists, runs proposer-optimal Gale–Shapley, and then independently checks every mutually acceptable pair for blocking. GAME.CONGESTION keeps named resource incidence compact, records every strict best-response update, certifies the corresponding decrease in Rosenthal's potential, and checks every final unilateral route change. All three return bounded work counts and concrete counterexamples where applicable.

Finite incomplete-information normal form uses an explicit joint prior:

game SignalingStage { bayesian = BayesianSpecification }
BayesianEquilibrium = GAME.BAYESIAN(SignalingStage)

GAME.BAYESIAN requires every type profile in the prior and every type/action payoff row. It enumerates bounded type-contingent strategies, solves their two-player general-sum strategic form with the certified support enumerator, and returns both mixed plans and per-type behavioral marginals.

Discounted state games keep transitions explicit:

game RepeatedContest { stochastic = StochasticSpecification }
StationaryEquilibrium = GAME.STOCHASTIC(RepeatedContest)

Each state defines row and column actions and one immediate-reward/transition record for every action pair. GAME.STOCHASTIC solves the Shapley continuation matrix at every state, normalizes accepted transition mass while retaining its input residual, and iterates only within authored state-action and iteration budgets. The result includes stationary mixed strategies, independent maximin/minimax matrix certificates, a Bellman residual, and global value and policy error bounds derived from the declared discount contraction. Discounts must be below one; undiscounted average-reward games are not silently treated as discounted games.

Declarative mechanisms

mechanism Auction {
  direct = DirectSpecification
}
 
Audit = MECHANISM.AUDIT(Auction)
Truthful = MECHANISM.VERIFY(Auction, "dsic")

The block lowers to MECHANISM.DIRECT(DirectSpecification). A direct specification contains ordered agents and types, one outcome for every report profile, an outcome id, one payment per agent, and an agent-by-true-type utility matrix. An optional complete joint prior enables Bayesian checks.

MECHANISM.AUDIT exhaustively checks DSIC, ex-post individual rationality, no deficit, and strong budget balance. When a prior is present it also checks BIC and interim individual rationality. MECHANISM.VERIFY selects dsic, bic, ex_post_ir, interim_ir, no_deficit, or strong_budget_balance and returns either supporting metrics or the concrete misreport, participation, or budget counterexample.

MECHANISM.VCG_ASSIGN computes an exact welfare-maximizing unit-demand matching, one Clarke-pivot counterfactual per winner, payments, utilities, and IR/no-deficit evidence. General finite feasible sets use:

mechanism Allocation { vcg = FeasibleOutcomeValues }
Result = MECHANISM.VCG(Allocation)

MECHANISM.VCG chooses the welfare-maximizing enumerated outcome and returns one Clarke-pivot externality payment, counterfactual outcome, and utility certificate per agent. This covers combinatorial and public-choice domains when their feasible alternatives are enumerated. GAME.AUCTION resolves deterministic first- and second-price single-item auctions with reserve pricing and stable tie-breaking.

Graph, Predicate, and WHY

Resident Graph handles project directly into both complete normal-form games and compact local-payoff factor games. Discounted stochastic games have a third closed projection: a game node owns its two players and states, states own their local actions and outcomes, and probability-bearing transition edges retain the dynamic topology directly. Projection and solution pin the same immutable Graph revision and fingerprint; stochastic iteration and state-action work have dedicated process telemetry.

The compact graphical-game bridge preserves factor scope, never materializes the global payoff product, pins the exact Graph revision/fingerprint, and retains equilibrium certificates per connected strategic component. A local payoff-property patch therefore recomputes only the component that can observe it; unchanged components reuse their proofs. Projection scans and strategic recomputation have separate telemetry.

GAME.NORMAL_FORM also accepts ordinary arrays, so collected Frame rows and Graph query results remain first-class dependencies when an authored workbook wants to shape the relation itself. A Predicate publication can consume GAME.VERIFY(...).passed, while the complete returned object retains its witness. Typed game/mechanism results attach a strategic proof snapshot to their ordinary WHY node: claim, pass/refute polarity, tolerance, metric, counterexample, solver certificate, and work counts remain structural inside the same provenance tree as Predicate proof steps.

When authored source needs to reshape graph relations itself, the explicit relation bridge remains a typed Frame projection and bounded collection:

frame StrategyFrame = SELECT player, strategy
  FROM GRAPH_EDGES(StrategicModel)
 
Strategies = COLLECT(StrategyFrame, {limit: 10000})

The same shape works for MODEL.PREDICATES: project the relevant predicate edges with GRAPH_EDGES, select their identity/payload columns, and COLLECT under an authored bound. The resulting rows may feed players, strategies, or payoffs in a game block. Graph revision, Frame plan, collection bound, and game constructor are then one dependency chain; a predicate membership or edge-property edit invalidates the strategic result normally.

Keep the evidence object rather than projecting only its boolean when the model must explain failures. A failed pure-Nash claim identifies a profitable deviation; a failed incentive claim identifies the agent, true type, report, deviation, utilities, and regret.

Limits and compatibility

• epsilon, maxProfiles, maxDeviations, solver limits, contingent-plan, coalition, tree-evaluation, potential-update, and counterfactual limits are authored bounds.
• Invalid/incomplete domains produce #VALUE!; exhausted analysis or solver budgets produce #NUM!.
• Strategic input contracts reject unknown fields. Imperfect-recall trees, continuous type spaces, or other undeclared capabilities cannot be silently discarded and reinterpreted as a simpler certified model.
• Existing GAME = ... and MECHANISM = ... bindings remain legal; a keyword is treated as a declarative block only when followed by a name and {.
• Existing function calls remain the canonical compatibility surface. The blocks are optional syntax over those calls.
• Imperfect recall, general-sum imperfect-information trees, and unbounded/continuous strategy spaces are not approximated by the certified finite lanes.

See the generated function catalog for signatures and predicates.md for evidence publications and logical inference.