A Formal Notation for Floor Plans

The governed-kernel architecture that Chapter 6 delivered is complete as a specification and incomplete as a representation, and the gap between those two conditions is the work this chapter takes up. A nine-type module taxonomy, a stratified entity vocabulary of seven primitives and seven composites, a ten-operator relation layer, and a set of constituent and interaction rules together fix what an accessible dwelling plan means; they do not yet fix how that meaning is written down so that a machine can read it, compose with it, and check it. The grammar supplies that missing layer. It is, in the terms the thesis uses of its own evidence machinery, the notation under which the modularity engine becomes inspectable, parseable, and transformation-safe — the form in which the architectural claim developed across the artefact suite can be verified rather than merely asserted. The engine itself is not built here and its decisive demonstration is not staged here; Chapter 6 specifies the engine and Chapter 10 demonstrates it at a single fork. What this chapter owes is a representation in which the engine’s commitments can be expressed without loss and audited without re-interpretation.

Receipt of the governed kernel

Chapter 6 transmits the governed-kernel architecture through four formal handoff contracts, and each fixes a boundary on what this chapter may do with the material it receives. Handoff Contract HC-6A transmits the four-layer governed kernel — the stratified entity vocabulary (seven primitives and seven composites), the ten-operator relation layer, the nine-type module taxonomy, the thirty-two hard and eleven soft constituent constraints, and the three-type inter-module interaction rules — to be formalised in any notation that preserves semantic equivalence with the prose-and-table specifications, without adding vocabulary terms, revising type definitions, or resolving an ambiguity unilaterally. HC-6B transmits the twenty-five baseline library entries as the notation’s test material: a notation expression must produce valid representations of all twenty-five without violating a governed-kernel contract. HC-6C transmits the verification-sequence constraint — primitive-plane modules before configurative-plane modules, configurative before the dwelling aggregate — and asks that the grammar make violation of that order impossible in a well-formed plan. HC-6D transmits the three interface-type contracts (semantic, transformation, verification) as expressibility requirements the formal grammar must satisfy.

The four contracts are receipts rather than abstractions: each names a structural feature of the governed kernel that the notation developed in Sections 7.3 through 7.20 must satisfy by an identifiable mechanism. The table below traces each contract’s requirement, drawn from Chapter 6, Section 6.5 and the specifications it consolidates, to the mechanism that discharges it here and to the experimental record that audits the discharge. Where the audit returns a partial verdict, the table flags the partial status rather than absorbing it into a generic pass.

A second inheritance bears on what the notation may denote. Beyond the governed kernel’s four layers, this chapter inherits the governed triplet substrate that Chapter 5 delivered: 611 governed text-clause representations and 189 governed figure-derived representations in subject–predicate–object form, each carrying a stable record identifier, a governed clause class, a confidence-labelled ambiguity profile, and a residual flag with a declared disposition. Because Chapter 6’s vocabulary, taxonomy, and rules were themselves derived from that substrate, the notation developed here is, by way of Chapter 6, the formalisation of an entity–relation–property structure that originates in corpus evidence rather than in analyst intuition. The connection fixes three things at once: what the notation’s terminal symbols denote (entities and relations grounded in the corpus); what the notation cannot denote without a substrate revision (any primitive or relation absent from the closed stratified vocabulary and ten relation operators); and what residuals it carries forward unchanged — the fifty-four fallback-flagged terms, the twenty-nine other-class clauses, and the fifteen mixed-force clauses inherit from Chapter 5 through Chapter 6’s handoff under HC-6A’s no-modification clause.

The representational gap

Three capabilities the governed kernel lacks define the gap a formal notation must close. First, the specification cannot be tokenised: its elements are written in natural language, tables, and structured prose, so a machine process cannot find the boundary of a module definition, tell a primitive from a relation, or judge whether a constraint is met without first interpreting English sentences. Second, it cannot be parsed: even were the tokens identifiable, no grammar relates them, and the hierarchical structure of a plan — primitives composed into modules, modules into a dwelling aggregate — exists as a described principle rather than a syntactic rule. Third, it cannot guarantee transformation safety: the interaction rules describe how a plan may change under adaptation, but they describe it in prose, and a machine cannot confirm that a proposed change preserves the thirty-two hard constraints without re-reading and re-interpreting the constraint text. These three absences — no deterministic tokenisation, no compositional grammar, no checkable transformation logic — are what the notation supplies. The governed kernel provides the semantic content; the notation provides the syntactic and structural machinery that makes that content machine-operable.

The chapter’s claims

The chapter’s primary proposition is Proposition 3 (manipulability), executable transformation grammar with invariant checks: formal expressibility must become executable transformation logic rather than static notation alone, a language that expresses named transformations, preserved invariants, and admissibility conditions in a form that can be inspected, replayed, and verified.⁵ On our reading the chapter also bears, locally, on Proposition 5 (integrated utility), through the separation-of-concerns that the two-layer architecture preserves. Seven claims discharge these propositions. Claim C7-1 holds that the notation enables machine-operable representation and parsing — the capability logically prior to everything Proposition 3 requires. Claim C7-2 holds that the two-layer architecture preserves separation of concerns while enabling extensibility, and it is this claim that attaches to Proposition 5. Claims C7-3 through C7-7 are the Proposition 3 evidence base: C7-3, that RecPol satisfies all five Goodman notational criteria and so qualifies as a strict notation capable of the determinacy “executable” requires; C7-4, that the thirty-two hard constraints are preserved and machine-verifiable; C7-5, that the verification sequence is grammatically enforced; C7-6, that the three interface types are formally expressible across module boundaries; and C7-7, that round-trip fidelity is guaranteed by the grammar’s design. The remainder of the chapter develops these claims: Section 7.2 presents the two-layer architecture and the wrapping functor that binds its layers; Section 7.3 specifies RecPol, the formal core; Section 7.13 specifies PlaniSyn, the applied grammar; and Section 7.20 demonstrates the notation end-to-end and consolidates its contributions. The complete production rules and verb inventories are carried in the RecPol Specification appendix (RecPol) and the PlaniSyn Grammar appendix (PlaniSyn); the body develops the argument.

Thirteen inherited commitments

Two families of commitment, both inherited from Chapter 3, fix what a representational format must do to be governance-capable, and together they are the criteria against which the notation is designed. The first family is the eight text serialisation properties. Discreteness requires spatial entities to be represented as countable objects on an integer grid rather than as continuous coordinates, so that equality is decidable and configurations admit a finite representation. Composability requires larger structures to be built from smaller ones by explicit operations encoded in the text itself. Stability requires an entity’s representation not to change when its context changes — the property that, at the grammar level, is context-freeness. Diff-ability requires two representations to be comparable token by token, which in turn requires a canonical form. Versionability requires explicit version metadata. Parsability requires deterministic parsing in linear time, with no backtracking and bounded look-ahead, which constrains the grammar to be at most LL(k) for a small k. Semantic determinacy requires every token to map to exactly one interpretation. Round-trip fidelity requires that encoding a configuration, decoding the text, and re-encoding return the original text, which requires canonical normalisation. The second family is Goodman’s five notational criteria — syntactic disjointness, syntactic finite differentiation, semantic unambiguity, semantic disjointness, and semantic finite differentiation — the threshold conditions under which a symbol system qualifies as a strict notation rather than a general-purpose language.⁶ These thirteen commitments are not design preferences to be traded against convenience; they follow from the thesis’s concern with diachronic governance — the capacity to maintain meaning, verify compliance, and accommodate change across the handovers in a dwelling’s lifecycle — and a format that fails any of them cannot support the governance functions the module system was built to enable.

Why existing formats do not serve

The representational formats already available in the building-information domain were engineered for exchange, and exchange-adequacy and governance-adequacy turn out to be different goals that demand different representational architectures. The Industry Foundation Classes (IFC, ISO 16739) provide a rich entity-relationship model that satisfies parsability and composability, but the same design choices that make IFC a successful exchange format defeat it as a governance notation: its identifiers serve several syntactic roles by context (failing syntactic disjointness), its open-ended property sets take string-typed values whose equality cannot be decided without external ontology lookup (failing semantic finite differentiation), its entity references are instance-bound (failing stability), and its multiple geometric representations admit no canonical mediation (failing round-trip fidelity).⁷ The Green Building XML schema (gbXML), built for energy analysis, fails composability through a flat spatial model, semantic and syntactic disjointness through ambiguous element typing, stability through global-coordinate dependence, and round-trip fidelity through floating-point rounding.⁸ Ad hoc constraint schemas — the JSON configurations, spreadsheet rule engines, and bespoke databases of accessibility compliance tools — solve immediate operational problems but provide no formal grammar, no cross-version stability, and no formal symbol system. None of these is poorly engineered; each is highly engineered for the goal it was set, and that is precisely the difficulty: a substrate that meets the exchange goal cannot be silently retargeted at the governance goal.

A second class of candidate substrate, the description-logic family, warrants explicit examination because it appears, at first inspection, to satisfy several criteria that defeat the exchange formats: the Web Ontology Language profiles and their lighter relatives provide formally specified syntax, model-theoretic semantics, decidable reasoning, and a closed-vocabulary discipline. The surface fit conceals a tractability problem that the chapter’s Design Constraint DC-4 — that routine governance operations must remain within polynomial-time decidability and practitioner cognitive capacity — makes decisive. Full OWL 2 DL subsumption is doubly exponential in the worst case, and the fragment underlying practical reasoners is exponential; the tractable profiles regain polynomial behaviour only by surrendering the qualified-cardinality, role-composition, and bilateral-constraint expressivity that the governed kernel’s interaction rules and constituent specifications require, and the constraint language SHACL loses its tractable-validation guarantee precisely on the recursive bilateral constraints the substrate must support.⁹ A grammar-based notation meets DC-4 instead by construction: an LL(1) context-free grammar parses in linear time with single-token look-ahead, a three-level entity stratification bounds reference depth, a closed verb registry makes per-predicate verification a constant-time look-up, and a finite cascade bound makes verification terminate in linear rather than open recursion. The tractability is a structural property of the grammar’s formal class, not an empirical observation about typical ontology sizes, and it is the principled reason a description-logic substrate was set aside at the design-criteria stage and a grammar was developed in its place.

The governance-adequacy principle and the design criteria

The exchange-versus-governance distinction is worth naming, because the failure analysis cannot otherwise be summarised without circularity. We state it as the Governance Adequacy Principle: a representation system meets the governance-adequacy threshold if and only if it supports both lossless representation exchange between actors and computable verification of normative compliance against an external standard, where the second condition requires representational features the first does not entail. Exchange-adequacy and governance-adequacy are therefore non-equivalent; the latter strictly extends the former with the constraint-imposition machinery that exchange formats are designed to avoid imposing. The distinction is not peculiar to building information. It recurs wherever a community has had to separate data-transfer from constraint-imposition: Fielding’s architectural-style argument that constraints trade one property for another, and Garlan and Shaw’s contrast between data-flow and rule-based styles, both make the same structural point at the level of system organisation.¹⁰ On our reading the principle is the housing-governance instance of a long-standing insight that representational systems are style-bound, and that selecting an exchange-style substrate for a governance-style task is an architectural category error rather than a tractable refinement.

The design criteria for the notation follow directly from the thirteen commitments, organised into four groups. The syntactic criteria require a context-free grammar with single-character delimiters that partition every token into disjoint syntactic classes and a deterministic classification procedure for every mark, parseable LL(1) with single-token look-ahead. The semantic criteria require each token to map to exactly one interpretation, distinct tokens to denote distinct things, any two denotations to be distinguishable by a bounded procedure, and the vocabulary to be closed, with no open-ended property definitions or string-typed semantic values. The structural criteria require hierarchical composition to be encoded syntactically, the substrate to be a discrete integer grid, and the compositional hierarchy to mirror the module system’s three-plane structure. The fidelity criteria require a canonical form for every representable configuration, explicit version metadata, and an injective normalisation under which semantically distinct configurations produce distinct token sequences and identical configurations produce identical ones. These four groups are the specification the notation of the following sections must satisfy; they are not a wish-list but the conditions the theoretical framework imposes on any representational substrate for governed modular housing plans.

Navigation: ← Chapter 6: A Governed Kernel Architecture for Housing | ↑ Chapter 7 | 7.2 Notation Architecture and the Wrapping Functor →

A notation that must serve both a domain-independent geometric substrate and a domain-specific dwelling vocabulary faces a choice of architecture before it fixes any production rule, and the choice the design criteria of Section 7.1 force is a separation into two layers. The case for that separation rests on two independent arguments, one from modularity theory and one from the thesis’s own extensibility requirement.

The case for layered architecture

The modularity argument derives from Parnas’s information-hiding principle.¹¹ A monolithic grammar that merged geometric-substrate operations with dwelling-specific vocabulary would expose every downstream consumer to both at once, so that a change to the dwelling vocabulary — adding a module type for a future revision of the accessibility standard — would force re-verification of the geometric operations, even though those operations are domain-independent. Separating the layers confines vocabulary change to the applied grammar and geometric change to the formal core; each layer’s internal structure is hidden from the other, and the only traffic between them passes through a single declared interface. This is the information-hiding axiom of the modularity framework that Chapter 3, Section 3.3 established, applied to the notation’s own construction.

The extensibility argument is specific to what the thesis contributes. The geometric substrate of the formal core encodes operations on rectangular polyominoes that are not particular to dwelling plans; the same substrate could in principle govern warehouse layout, hospital-ward planning, or any spatial-governance problem posed over rectilinear compositions on a discrete grid. Fused with the dwelling vocabulary, that reuse would require extracting and refactoring the geometric operations; separated, the reuse is explicit, because any domain-specific applied grammar can be defined over the formal core without modifying a single core production. The two arguments are complementary — information hiding stops change in one layer from propagating to the other, extensibility lets further applied grammars be built without weakening the core’s formal guarantees — and together they justify Claim C7-2: the two-layer architecture preserves separation of concerns while enabling extensibility. A reasonable objection is that a single unified grammar would be simpler and avoid the mapping between layers; the rebuttal, developed below, is that the mapping is structure-preserving and so the separation is not arbitrary overhead but the mechanism that secures the chapter’s three formal claims.

The two layers

The formal core is RecPol (Rectangular Polyomino Language): a serialised, human-readable, modular formal language for defining and manipulating rectangular polyominoes on a discrete integer grid, governed by eight design axioms — discrete-spatial, serialised, uniform outer syntax, context-free, modular, stratified, bounded, and extensible — that Section 7.3 specifies in full. The applied layer is PlaniSyn (Planimetric Syntax): the grammar that binds RecPol’s abstract constructs to the governed kernel’s dwelling vocabulary, structured as three layers mirroring the planimetric triad of grid, place, and movement — a Declaration Layer for object identity, geometry, and properties; an Interaction Layer for four typed relationships between objects; and a Composition Layer for the hierarchical nesting that mirrors the near-decomposable structure of a dwelling plan. The two layers and the functor that connects them are shown in Figure 7.1; Section 7.13 specifies PlaniSyn in full.

The wrapping functor

The relationship between the two layers is a wrapping functor, written W: G → A, from the set G of RecPol geometric constructs to the set A of PlaniSyn applied-grammar constructs. The functor preserves three properties. It is a faithful representation: every RecPol construct that participates in the dwelling domain has a unique PlaniSyn counterpart, so the mapping is injective within that domain. It is semantically derivable: every PlaniSyn semantic assertion follows from the composition of RecPol operations and the functor’s vocabulary binding, with no assertion that requires a mechanism outside RecPol. And it is compositional: when two RecPol constructs compose into a larger one, their PlaniSyn images compose into the corresponding expression, so hierarchical structure is preserved. The functor performs a narrowing, not a lateral translation. RecPol can represent any configuration of rectangular polyominoes on a discrete grid; PlaniSyn represents only those configurations that also conform to the governed kernel’s module types, constraint structures, and interaction rules. The functor adds semantic constraints, narrowing the well-formed expressions from all geometrically valid RecPol documents to those that additionally satisfy the thirty-two hard constraints and the three interface-type requirements. This narrowing is the mechanism by which the notation preserves the governed kernel’s semantic contracts and so discharges Claim C7-4: a PlaniSyn expression is well-formed if and only if its RecPol substrate is grammatically valid and its applied-grammar bindings satisfy the governed-kernel contracts, so that validity at the lower level guarantees geometric soundness and validity at the upper level guarantees semantic soundness.

Calling the map a functor is more than a metaphor, and the claim earns the term in a deliberately bounded sense. The desugaring discipline that defines the applied grammar — every PlaniSyn construct desugars to a determinate sequence of formal-core entity blocks, applied-grammar identifiers adopt the formal-core identifier production, and the formal core is never modified — makes the map satisfy the two functor laws by construction: the empty PlaniSyn extension desugars to the empty token sequence (identity preservation), and the desugaring of a composite distributes over its parts under the strict left-to-right evaluation rule (composition preservation).¹² The point of the term is modest and precise: the binding between layers is structure-preserving, so collapsing the architecture into a unified grammar would not remove overhead but would lose the separation that the kernel specifications of Section 7.3 exploit to resolve the design-axiom tensions, and that the extension-point discipline relies on to preserve Goodman compliance under future extension.

Semantic contracts between the layers

Five semantic contracts govern what the applied grammar may and may not do relative to the formal core, and they are the interface specification between the layers in the same sense that the interface contracts of the module system govern its boundaries. Contract SC-1 (core immutability) forbids PlaniSyn to modify any RecPol production, terminal, or semantic definition: the formal core is read-only from the applied grammar’s side. Contract SC-2 (extension-point discipline) permits PlaniSyn to introduce domain-specific tokens only through the six reserved extension-point tokens, which is what preserves the core’s LL(1) parsing guarantee under extension. Contract SC-3 (plane-assignment compliance) requires every PlaniSyn entity to be assigned to exactly one RecPol plane through the projection operator, consistently with the governed kernel’s module-type classification. Contract SC-4 (verification-sequence preservation) requires the primitive-before-configurative-before-interactive ordering inherited under HC-6C to be preserved, so that a well-formed document cannot reference a higher-plane entity from a lower-plane block. Contract SC-5 (semantic equivalence with the governed kernel) requires every governed-kernel element — the stratified entity vocabulary, the ten relation operators, nine module types, thirty-two hard constraints, and three interface types — to be expressible in PlaniSyn without loss of content, and requires that any ambiguity the formalisation reveals in the governed kernel’s prose be flagged for resolution in Chapter 6 rather than resolved unilaterally in the applied grammar, which operationalises HC-6A. Taken together the five contracts ensure that the extensibility the two-layer architecture enables does not come at the cost of semantic integrity; they are the conditions under which the narrowing functor of Section 7.2 can be trusted to carry the governed kernel’s commitments intact into the dwelling domain.

Navigation: ← 7.1 Introduction and the Need for Formal Notation | ↑ Chapter 7 | 7.3 RecPol: The Formal Core →

RecPol is the domain-agnostic formal core on which any applied grammar is built: a serialised, human-readable language for defining and manipulating rectangular polyominoes on a discrete integer grid, carrying no dwelling-specific vocabulary of its own. Its design space is constrained by eight axioms, each traceable to the requirements consolidated from the governed kernel and justified by the theoretical framework of Chapters 2 and 3, and the specification that follows is organised around them.

7.4 Design axioms and their consistency

The eight axioms are presented in their frozen form. DA-01 (discrete-spatial) fixes the substrate as an orthogonal integer lattice whose atomic units are cells and whose inhabitants are rectangular polyominoes; no real-valued coordinates appear, because a continuous space admits configurations that no bounded procedure can distinguish and so would violate both of Goodman’s finite-differentiation criteria. DA-02 (serialised) expresses every language element as a linear token stream in subject–verb–object form, with a canonical orthography that makes round-trip fidelity a consequence of determinism. DA-03 (uniform outer syntax) declares every entity through the single form < identifier | predicate_list >, so a parser can find an entity’s boundary without knowing its type — a precondition for single-token-look-ahead parsing. DA-04 (context-free) makes RecPol a Chomsky Type 2 grammar in which each entity block is parseable without reference to any other, which secures the stability criterion of Section 7.1. DA-05 (modular) provides first-class boundary and interface declarations, three syntactically distinguished interface types, and the applied-grammar extension contract. DA-06 (stratified) defines exactly three planes — Primitive (invariant geometry), Configurative (relational geometry), and Interactive (concrete placement) — and makes the verification sequence a structural property of the grammar rather than a runtime check.¹³ DA-07 (bounded) forbids left-recursive cycles and requires entity reference graphs to be acyclic, so that parsing, verification, and generation terminate in finite steps. DA-08 (extensible) provides formally specified extension points — the wrapping functor of Section 7.2 — through which applied grammars introduce domain-specific tokens without modifying any core production.

The eight axioms are necessary, independent, and mutually consistent, and the two tensions that might appear to threaten consistency are resolved by named mechanisms rather than by relaxing an axiom. The first tension is between DA-04 and DA-05: bilateral interface constraints — those whose evaluation requires inspecting two module instances at once, such as a coupling whose validity depends on aligned openings on both sides of a shared boundary — appear to demand the non-local context that context-freeness forbids. The resolution is a post-parse semantic pass. The LL(1) parser admits each entity block in isolation under DA-04 and produces a complete parse tree without consulting any other block; a separate pass then traverses the populated world-model state and evaluates the bilateral constraints whose two endpoints have both been registered. The parser remains Type 2 and keeps its linear-time guarantee, because the semantic pass operates on the symbol table and relation store rather than on the token stream. The second tension is between DA-04 and DA-06: the verification sequence imposes a global ordering that a context-free grammar cannot carry. The resolution is a two-pass verification algorithm — a purely syntactic first pass that populates the world model without inspecting plane assignments, and a semantic second pass that walks the entity registry in stratum order (Shape entities, then Form, then Instance) and rejects any cross-stratum reference that violates the strictly descending direction. Two passes are required rather than one because no LL(1) parser can decide, mid-stream, whether a forward reference will resolve to an entity at a permitted plane; that decision needs the symbol table to be complete. Splitting parsing from verification also preserves modular fit, since a future revision to the plane-ordering rule would modify only the second pass, leaving the grammar and its productions untouched.

7.5 World model and coordinate systems

The world model has three elements: a discrete lattice of cells, rectangular polyominoes as the inhabitants of that lattice, and three coordinate systems for addressing positions at different scales. Cells are atomic unit squares whose only properties are an integer position and an occupancy state; every spatial operation reduces to operations on finite sets of cells. Rectangular polyominoes are finite, edge-connected, axis-aligned cell sets (or unions of axis-aligned rectangles, for composites), and they are the named, plane-typed subjects of the language. Three nested coordinate systems address positions at the three scales the stratification distinguishes: a cell index local to an entity’s bounding box (with a zero-exclusion convention that eliminates off-by-one boundary errors), a world grid over the integers for global placement, and a signed edge index that addresses perimeter edges with orientation for adjacency detection, opening placement, and perimeter-constraint evaluation. The nesting mirrors the three-plane stratification — Primitive-plane entities use cell indices, Configurative-plane entities use bounding-box-relative positions, and Interactive-plane entities use world-grid coordinates.

7.6 Entity type system and plane projection

RecPol defines three entity types, one per plane, assigned by the plane projection operator (^): s^A denotes a Shape on the Primitive plane, carrying the invariant cell-set geometry of a polyomino; f^A denotes a Form on the Configurative plane, binding Shapes into relational structures by importing their geometry, applying local transformations, and declaring constraints; and i^A denotes an Instance on the Interactive plane, placing Forms on the world grid under global transformations. The type system enforces the verification-sequence constraint (Claim C7-5) structurally rather than by a runtime check. A Shape has no predicate vocabulary with which to reference a Form or Instance; a Form may reference Shapes but not Instances; an Instance may reference Forms and other Instances, but only downward, importing a complete specification without modifying it. A parser that meets a Shape referencing a Form rejects the document as ill-formed before any semantic evaluation begins, which is how the grammar discharges Handoff Contract HC-6C: entities on a lower plane simply lack the means to reference a higher one.

7.7 The complete EBNF

The RecPol formal syntax is a nineteen-production LL(1) grammar over twelve terminal token types — OPEN_ENTITY (<), CLOSE_ENTITY (>), OPEN_PRED ([), CLOSE_PRED (]), PIPE (|), SEMI (;), COMMA (,), COLON (:), CARET (^), MINUS (-), WORD, and INTEGER — together with six extension-point tokens ((, ), {, }, ., @) that the formal core declines to consume, reserving them for applied-grammar use. The grammar is presented here in Extended Backus–Naur Form; the full derivation and verification are in the RecPol Specification appendix.

P-01:  document       ::= entity_block*
P-02:  entity_block   ::= OPEN_ENTITY identifier PIPE predicate_list CLOSE_ENTITY
P-03:  identifier     ::= namespace CARET name_stem
P-04:  namespace      ::= WORD
P-05:  name_stem      ::= WORD
P-06:  predicate_list ::= predicate predicate_tail | EMPTY
P-07:  predicate_tail ::= SEMI predicate predicate_tail | SEMI | EMPTY
P-08:  predicate      ::= OPEN_PRED verb argument* CLOSE_PRED
P-09:  verb           ::= WORD
P-10:  argument       ::= number_start_arg | word_start_arg | minus_start_arg
P-11:  number_start_arg   ::= INTEGER coord_or_int
P-12:  coord_or_int       ::= COMMA INTEGER coord_tail | EMPTY
P-13:  coord_tail         ::= COLON INTEGER COMMA INTEGER | COMMA WORD edge_facing | EMPTY
P-14:  edge_facing        ::= COMMA WORD | EMPTY
P-15:  word_start_arg     ::= WORD word_suffix
P-16:  word_suffix        ::= CARET WORD | EMPTY
P-17:  minus_start_arg    ::= MINUS INTEGER coord_or_int_neg
P-18:  coord_or_int_neg   ::= COMMA integer_value coord_tail | EMPTY
P-19:  integer_value      ::= MINUS INTEGER | INTEGER

The grammar has nineteen non-terminals with complete referential closure and no undefined non-terminal. It is LL(1)-compatible: all eleven decision points have pairwise disjoint FIRST sets, so a single token of look-ahead suffices for deterministic parsing, and the one right-recursive production (the predicate tail, P-07) supplies variable-length predicate lists without left recursion.¹⁴ Three ambiguity tests conducted during development — distinguishing a verb keyword from an entity reference, a coordinate pair from a standalone integer, and nested entity references bounded by their delimiters — each confirmed that the grammar yields a unique parse tree for every well-formed input. The LL(1) property guarantees parsing in time linear in the number of tokens, with no backtracking, implementable as a simple recursive-descent procedure.

7.8 Canonical orthography

The canonical orthography is the unique textual form to which every representable configuration normalises, and it is the mechanism by which RecPol satisfies round-trip fidelity (Claim C7-7) and diff-ability. Its rules fix case conventions (verbs case-insensitive, namespaces and name stems case-sensitive), whitespace (three-space predicate indentation, single inter-token spaces, no tabs — cosmetic normalisation to byte-identity), symbol ordering (predicates ordered lexicographically by verb, arguments in positional-then-lexicographic order, which removes permutation ambiguity), and encoding (UTF-8, no string literals, a closed token vocabulary). These rules induce invariant INV-P-03: two configurations that are geometrically and relationally equivalent produce byte-identical canonical token sequences, and conversely any token difference signals a geometrically distinct configuration. That biconditional is the formal basis of round-trip fidelity and diff-ability alike.

7.9 Three-plane verb systems

RecPol’s verbs are stratified by plane. Primitive-plane verbs operate on cell sets: MakeShape creates a base rectangular polyomino from a width and height; MakeComposite fuses two Shapes along aligned edge segments into an L-shaped or more complex polyomino; and EdgeRun selects a contiguous, translation-invariant perimeter segment by a canonical clockwise walk. Configurative-plane verbs operate on members and constraints: CallShape imports a Shape’s geometry into a Form; MakeCompound groups members without geometric fusion; the local transformations (TransPosition, TransPivot, TransReflect, TransScale) reposition, rotate, reflect, or scale members non-commutatively; and the two constraint verbs, ConsLatchment (declaring whether an edge segment must, may, or must not be shared) and ConsOccupancy (declaring overlap tolerance with additive arithmetic within lanes and conjunctive evaluation across them), govern inter-member relations. Interactive-plane verbs operate on world-grid placements and generative parameters: CallForm and CallInstance instantiate; the identity-preserving global transformations (Place, Rotate, Mirror, Stretch) position and orient Instances without altering their structural properties; and StretchFit and the Range family supply the generative vocabulary developed below. No verb crosses a plane boundary, which is the syntactic consequence of DA-06 and the direct support for verification-sequence enforcement.

For independent evaluation, four primary kernel operations are specified in the structured pre/post/effect form drawn from the semantic-specification programme; the operationally named composite verbs (MakeComposite, ConsLatchment, ConsOccupancy) reduce to the formal-core verb registry’s canonical primitives by the procedures recorded in the experiment files.

Six cross-cutting invariants, each traced to the axiom that guarantees it, state the compliance surface every well-formed RecPol document must satisfy and that any conformant implementation or applied grammar must respect.

The register is jointly sufficient — every well-formed document satisfies all six, and a document violating any one is rejected under Strict conformance or flagged under Lenient — and exhaustive within this chapter’s scope, the plane-specific Configurative and Interactive invariants being recorded in the experiment files and referenced from the RecPol Specification appendix.

7.10 Version semantics

To support change control over the long governance horizon, every grammar element is assigned to one of three version-semantic classes. Governed-kernel elements — the nineteen productions, the twelve terminals, the verb registry, the eight axioms, the semantic specifications, the invariants, the orthography rules, and the error taxonomy — may not change without breaking RecPol’s identity as a notation; any modification is a breaking change requiring a major version increment and a re-issue of conformance verdicts. Version-annotated elements — metadata headers, comparison verdicts, iteration registers, and growing test-case rosters — may evolve under minor increments without invalidating earlier examples. Extension-point elements — the six reserved tokens and the registry, identifier-convention, generative-constraint, and error-taxonomy extension mechanisms — are non-breaking by construction. The classification is exhaustive: every element falls into exactly one class, and an applied-grammar extension is admissible only insofar as it operates within the extension-point class, with formal-core immutability guaranteed by the extensibility contract. The same taxonomy governs PlaniSyn (Section 7.13), so a single register binds both layers.

7.11 Generative constraints

RecPol’s constraint system extends beyond the static constraint verbs to generative constraints — parametric envelopes for automated design exploration. StretchFit adjusts an entity’s geometry to a target’s dimensions through four edge-specification types (cell-based and index-based edge runs, point-to-point, and wildcard) and supports dynamic targets specified by reference, enabling responsive layouts. The Range family (RangePlace, RangeFit, RangeRotate, RangeMirror, RangeStretch) restricts the parameter space of a transformation, serving both validation — where a transformation is admissible only if its parameters fall within the declared range — and generation, where the range defines the search space an automated generator may explore. The generative-constraint system is the mechanism by which the notation supports the procedural generation pipeline of Chapter 9: RecPol provides the parametric vocabulary, PlaniSyn the domain-specific bindings, and Chapter 9 the generation engine that operates within these bounds. Two conformance levels govern violation handling — Strict, where a violation is a hard error, for compilers and validators; and Lenient, where a violation triggers a warning, for runtime sandboxes.

7.12 Goodman compliance

RecPol’s claim to strict-notation status (Claim C7-3) rests on a formal gate that verifies all five of Goodman’s notational criteria, defined as inherited commitments in Section 7.1.¹⁶ Syntactic disjointness holds because the LL(1) grammar guarantees unique parse trees, its eleven decision points have pairwise disjoint FIRST sets, and the three ambiguity tests confirm that no input admits two parse trees. Syntactic finite differentiation holds because the parser classifies every expression in linear time with one token of look-ahead. Semantic unambiguity holds because all nineteen productions map to unique semantic constructs; the one technical challenge, the WORD token consumed at seven points, is resolved by production context, each consumption assigning exactly one sub-role. Semantic disjointness holds because every distinct concept has a distinct syntactic form. Semantic finite differentiation holds because the canonical-form mapping is injective under INV-P-03. The gate verdict is therefore 5/5 PASS, and RecPol qualifies as a strict notation in Goodman’s sense: a symbol system in which every mark is classifiable and every denotation determinable by bounded procedures.

The verdict carries an explicit limitation. The Goodman verification is an internal assessment: the properties invoked to satisfy each criterion are properties of the same artefact whose notational status is under evaluation, and the assessment was conducted by the notation’s designer rather than an independent evaluator. This is the same self-referentiality that the systemic evaluation of Chapter 5 declared of itself. The evidence for each criterion is structural — derivable from the grammar specification — rather than empirical, which strengthens the claim’s basis without eliminating the designer-assessor identity; an independent mechanised proof of the FIRST-set disjointness conditions, or a third-party parser generator producing zero-conflict output, would raise the assurance level, and we record that verification as future work. The 5/5 PASS should be read as a designer’s self-assessment against Goodman’s criteria, subject to the same declaration of limits that governs all internal evaluation evidence in this thesis. A further objection deserves direct reply: that Goodman’s criteria, developed for non-computational notations such as musical scores and dance, may not transfer to a formal grammar. The rebuttal rests on three grounds. Empirically, the full-grammar gate returns 5/5 by structural derivation from the grammar rather than by translating an aesthetic judgement into a technical setting. Philologically, the secondary literature affirms that the criteria apply to formal symbol systems by structural analogy rather than by domain accident. And structurally, the criteria are domain-agnostic by construction: they are statements about the syntactic and semantic identity conditions a notation must satisfy in order to function as a notation, and their origin in non-computational notations reflects the historical context in which they were first articulated, not a limit on their reach.

Navigation: ← 7.2 Notation Architecture and the Wrapping Functor | ↑ Chapter 7 | 7.13 PlaniSyn: The Applied Layer →

PlaniSyn binds RecPol’s abstract substrate to the dwelling vocabulary of the governed kernel. Where RecPol fixes geometry, PlaniSyn fixes what a configuration of that geometry means in an accessible dwelling — which module type it is, what it must contain, and how it may interact with its neighbours — and it does so entirely through the extension-point discipline of Section 7.2, adding no formal-core production.

7.14 Three-layer architecture

PlaniSyn is structured as three layers, each mapping to a representational function, a RecPol plane, and a dimension of the planimetric triad. The Declaration Layer specifies object identity, geometry, and properties as self-contained bracketed expressions — the PlaniSyn counterpart of a RecPol entity block, inheriting the context-free property so that a declaration is interpretable without reference to any other — and maps to the grid dimension, establishing the metric substrate. The Interaction Layer specifies four typed relationships between declared objects, asserted bilaterally, and maps to the movement dimension, encoding the patterns of access, adjacency, and containment that define a dwelling’s functional structure. The Composition Layer specifies hierarchical nesting, forming a recursive tree that mirrors the near-decomposable structure of dwelling plans, and maps to the place dimension.¹⁷ The three layers are not three notations bolted together; they are three facets of one system, connected by the wrapping functor and governed by the five semantic contracts of Section 7.2, jointly instantiating RecPol’s three-plane architecture and the near-decomposable governance model of Chapter 3.

7.15 Tag grammar and object model

PlaniSyn uses seven tag types to realise the three layers, each bound to a RecPol token to comply with Contract SC-2 (extension-point discipline): a Declaration Tag (< >, the entity-block counterpart, whose class separator partitions parameters into semantic groups); an Action/Iteration Tag ({ }, for interactions and nested declarations, using the reserved brace tokens); a Prerequisite Value Tag ([ ], for cardinality constraints and target identification); a Transformation Tag (( ), for geometric transformations, using the reserved parenthesis tokens); a Class Separation Tag (|, overloading the PIPE token with applied-grammar semantics); a Capital Parameter Tag (the named parameters P, B, D, A, O, An identifying each parameter group’s role); and a Lowercase Variable Tag (instance-specific values). The object model defines the nine module types of the governed-kernel taxonomy — ENT (entry), CIR (circulation), SAN (sanitary), BED (bedroom), LIV (living), KIT (kitchen), SVC (service), EXT (external), and DWL (dwelling aggregate) — each with a fixed primitive profile, cardinality bounds, and internal relation patterns inherited from Chapter 6, Section 6.2. Every object carries a stable referential identity: a persistent unique identifier that enables deterministic version control, cross-reference, and diff-based change tracking. The joint version semantics of the two layers is specified once, in Section 7.10; the PlaniSyn syntactic mechanisms developed below sit within the extension-point class of that classification by construction and need not be re-tabulated here.

The tag grammar binds RecPol’s substrate to the governed-kernel vocabulary surjectively: every term of the stratified entity vocabulary — seven schematic primitives and seven elaborated composites — and every operator of the ten-element relation-operator layer specified in Chapter 6, Section 6.1 has a distinct PlaniSyn syntactic realisation, with nothing collapsed or approximated by an extra-vocabulary construct. The two terms added under the cognitive primitive–composite–module re-stratification — the actor primitive and the within_context operator — require no new syntactic target: each is realised through a PlaniSyn form already in the grammar (the Prerequisite Value Tag keyword and the design-category context binding respectively), so the surjection extends to them by construction. Table 7.1 enumerates it and supplies the syntactic-level closure evidence for Claim C7-4.

Table 7.1. Governed-kernel stratified entity vocabulary and relation-operator layer mapped to PlaniSyn syntactic forms.

No term or operator is collapsed and no entry is approximated, so the closure is complete: the tag grammar supplies a representational target for every Chapter 6 vocabulary element, and the systematic use of the six extension-point tokens for PlaniSyn delimiters confirms that the applied grammar layers cleanly onto the formal core under the DA-08 contract, with no formal-core production overloaded.¹⁸

7.16 Spatial primitives

PlaniSyn encodes four categories of spatial primitive, each corresponding to a property domain of the governed kernel’s module specifications. The perimeter specification encodes a module’s outline as a closed loop of cardinal-direction movements and distances — P:N10 E8 S10 W8 traces a ten-by-eight rectangle — and corresponds to RecPol’s MakeShape, the movement sequence defining the cell set; non-rectangular outlines are traced by longer movement sequences. The border specification encodes wall thickness or clearance margin as an inset offset (B:1 for a uniform one-unit border, edge-specific values for a variable one) and corresponds to the governed kernel’s boundary primitive. The anchor specification encodes how a module connects to its context through a point anchor (absolute grid coordinates), an edge anchor (alignment to a named edge of another object), or a surface anchor (interior positioning within a container), corresponding to the governed kernel’s interface declarations. The opening specification declares doors, windows, and passages with identity, placement, sizing, and direction (O: D1@W3; W1@N5 placing a door three units along the west edge and a window five units along the north), corresponding to the opens_to relation; openings are the primary carriers of the coupling interaction, since a coupling requires aligned, bilateral opening declarations.

7.17 Interaction types and interface expressibility

PlaniSyn defines four interaction types that collectively realise the three interface types of the governed kernel, which is how it discharges Handoff Contract HC-6D. Engaging is shared boundary without traversal: a symmetrical adjacency, declared bilaterally by both modules, carrying a semantic interface (the shared boundary segment is the same entity in both module descriptions). Coupling is shared boundary with aligned openings: a symmetrical connection that extends engaging with a traversable aperture, requiring dimensionally compatible bilateral opening declarations, and carrying both a semantic interface (the shared opening) and a transformation interface (a change to one module’s opening dimensions must propagate to the coupled module). Entangling is one-sided penetration: an asymmetrical perimeter-to-interior interaction with a directed initiator, in which a penetrating component constrains the receiving module’s interior space, carrying a transformation interface through the directed declaration. Encasing is one-sided enclosure: an asymmetrical full containment expressed through the nesting syntax, in which the container’s perimeter constrains the contained module’s extent, carrying a verification interface whose localisation principle scopes verification results to the module boundary and whose cascade rule re-verifies a contained module when its container is verified.

For the formal verification Claim C7-6 requires, the interaction semantics is restated in the pre/post/effect form used for the formal-core kernels, where the preconditions are the conditions both participating modules must satisfy, the postconditions are the invariants the parser guarantees once the interaction is admitted, and the effects are the constraints propagated across the boundary.

Table 7.2. Pre/Post/Effect specification for the four PlaniSyn interaction types.

The two transformation-carrying types (entangling, encasing) activate the transformation interface’s admissibility and containment rules; the two symmetrical types (engaging, coupling) activate the semantic interface’s ownership and closure rules; and all four contribute to verification-interface activation through their lane membership.¹⁹

The complementary check — that every interface type is fully expressible by at least one interaction type, so that no HC-6D-mandated interface is left without a syntactic carrier — completes the four-to-three mapping.

Table 7.3. PlaniSyn interaction-type coverage of the three governed-kernel interface types (HC-6D).

The aggregate row is the explicit closure check Claim C7-6 requires: every interface type has at least one carrier and every interaction type carries at least one interface, so the four-to-three mapping is complete and non-redundant, and Handoff Contract HC-6D is satisfied at the syntactic-mechanism level.²⁰

7.18 Hierarchical nesting and the verification sequence

PlaniSyn encodes hierarchical composition through three-level recursive nesting corresponding to the three planes: Level 1 (Primitive) holds fixtures, openings, and path segments carrying invariant geometry; Level 2 (Configurative) holds the nine module types, carrying relational geometry and the four interaction types; and Level 3 (Interactive) holds the dwelling aggregate, carrying contextual properties. The nesting structurally encodes the verification-sequence constraint (Claim C7-5, discharging HC-6C): a well-formed document resolves all Level 1 entities before a Level 2 entity references them and all Level 2 entities before the Level 3 aggregate references them, enforced not by a runtime convention but by the grammar’s requirement that a referenced entity be declared within nesting scope before it is referenced.

7.19 Constraint preservation

The notation’s capacity to preserve the thirty-two hard constraints of the governed kernel (Claim C7-4) is realised by four grammar-level mechanisms integrated into the well-formedness conditions rather than layered on as a runtime checking pass. Mandatory-inclusion constraints — every BED module must contain at least one door — are encoded as cardinality assertions in the Prerequisite Value Tag ([D >= 1]), and a declaration that lacks the required element is rejected as ill-formed at declaration time. Conditional constraints — if a CIR module has a level transition it must have a handrail — are encoded as conditional prerequisite values ([IF level_transition THEN handrail >= 1]), mapping directly to the governed kernel’s IF–THEN form. Exclusion constraints — a SAN module must not contain a kitchen fixture — are encoded as zero-value cardinality assertions ([KIT_fixture = 0]). Cardinality constraints across the equality and inequality operators are encoded by the Prerequisite Value Tag’s integer operators. Bilateral interface constraints — a coupling requires matching opening declarations on both sides — are enforced by the bilateral declaration requirement of the coupling interaction, a one-sided declaration being syntactically ill-formed. Because the constraints are part of the grammar’s well-formedness conditions, a document that violates a hard constraint is not merely flagged but ill-formed, and the parser rejects it before any downstream processing, which is the syntactic expression of the governed kernel’s governance model that hard constraints are non-negotiable.

Navigation: ← 7.3 RecPol: The Formal Core | ↑ Chapter 7 | 7.20 Encoding, Validation, and Contributions →

A notation earns its claims only when it is exercised end-to-end on a configuration that stresses every mechanism it provides, so this section runs the encoding pipeline on a worked dwelling fragment, demonstrates round-trip fidelity, reports the requirements traceability, and consolidates what the notation contributes to the thesis and hands forward to Chapter 9.

7.21 The encoding pipeline

The composition method proceeds in eight steps, each mapping a representational task to a notation mechanism. First, the plan is decomposed into discrete spatial entities, each assigned a unique identifier and classified by one of the nine module types of Chapter 6, Section 6.2. Second, each entity receives a RecPol Shape declaration at the Primitive plane, its physical extent encoded via MakeShape or MakeComposite — the step at which the wrapping functor maps a dwelling entity’s geometry to a RecPol specification. Third, each entity’s primitive profile is asserted from the constituent-element specifications. Fourth, the ten relation operators are encoded as interaction declarations and property assertions — the structural relations mapping to the interaction types, the attributive relations to property parameters. Fifth, quality parameters are attached; the has_quality relation, which carries the largest share of triples in the SDA corpus, is encoded through the Capital Parameter Tags.²¹ Sixth, modality is declared: the thirty-two hard constraints become well-formedness conditions and the eleven soft constraints become advisory annotations. Seventh, the instance is validated against the twenty-five baseline library entries. Eighth, it is serialised to canonical text. The result is a deterministic, diff-able, versionable text representation of the plan.

7.22 A worked example: an L-shaped living–kitchen with a coupled service lane

The pipeline is best seen on a configuration that exercises cross-plane composition, an interaction declaration, and an applied-grammar generative constraint at once: an open-plan living and kitchen area in which the living module is an L-shaped composite of two rectangular Shapes, the kitchen module is a rectangular Shape coupled to the living module by a service-bench opening, and a StretchFit constraint declares the kitchen bench width as a parameterised range satisfying a minimum-clearance requirement.²² The composition takes five layered declarations: two Primitive-plane Shapes establish the L-shape’s two rectangular constituents; a Configurative-plane Form imports both via CallShape and positions the wing with a Translate; a second Form imports the kitchen rectangle and declares a StretchFit over its bench element; two Interactive-plane Instances place the two Forms and declare a lane between them with bilateral scope; and a coupling interaction is declared bilaterally with an aligned opening on each side of the shared boundary. The canonical text is:

< s^LIV_main | { MakeShape 1,1 : 5,4 } >

< s^LIV_wing | { MakeShape 1,1 : 3,3 } >

< s^KIT_box | { MakeShape 1,1 : 4,3 } >

< f^LIV_module |
    { CallShape s^LIV_main } ;
    { CallShape s^LIV_wing } ;
    { Translate 5,1 } ;
    { DeclSemIface s^opening_LK EXPORTED } ;
    { DeclTransIface ALL_ROTATIONS NO_REFLECTION }
>

< f^KIT_module |
    { CallShape s^KIT_box } ;
    { DeclSemIface s^opening_LK EXPORTED } ;
    { DeclTransIface ALL_ROTATIONS NO_REFLECTION } ;
    [ StretchFit bench_width 1200 ]
>

< i^LIV_01 |
    { CallForm f^LIV_module } ;
    { Place 5,5 } ;
    { Rotate 0 }
>

< i^KIT_01 |
    { CallForm f^KIT_module } ;
    { Place 12,5 } ;
    { Rotate 0 } ;
    { DeclLane i^LIV_01 i^KIT_01 1,1,W BILATERAL } ;
    { ConsBilateral OPENING_WIDTH_MIN i^LIV_01 i^KIT_01 } ;
    { DeclVerifIface i^LIV_01 CASCADE_NEXT }
>

The parse exercises the L-shape composition step by step. For the living Form, the parser admits CallShape s^LIV_main, initialising the composite extent to the twenty-cell main rectangle; admits CallShape s^LIV_wing, extending the import context to the nine-cell wing; and applies Translate 5,1 to the wing, so the two cell sets union without overlap into a twenty-nine-cell L-shape with an interior corner. The semantic-interface export and the admissible-transformation declaration seal the Form. The kitchen Form parses analogously, its fourth predicate [ StretchFit bench_width 1200 ] dispatching to the applied-grammar extension through the bracket extension-point tokens, where the verifier records a generative-constraint invocation that parameterises the bench width so the bench-to-opposing-fixture clearance is at least 1200 mm. The two Instances are placed on the world grid so their cell sets share a three-cell boundary segment — the geometric precondition for coupling — and the lane, bilateral opening-width predicate, and cascade declaration register the coupling’s verification obligations. The two-module coupling is realised by the conjunction of the bilateral opening export (satisfying the semantic interface’s closure rule), the bilateral lane (supplying the verification-interface scope), the bilateral opening-width predicate (exercising transformation-interface propagation should the opening width later change), and the applied-grammar coupling keyword admitted through the brace extension tokens. The document therefore exercises all three interface types on a single boundary, in service of one architecturally meaningful relation — an open-plan living–kitchen junction with an enforced minimum service-counter width — and its parse tree is unique, its re-serialisation deterministic, and its round-trip fidelity guaranteed by construction.

7.23 Round-trip fidelity

Round-trip fidelity (Claim C7-7) requires that encoding a configuration, decoding the resulting text, and re-encoding produces the original text. For a bedroom module declared with a four-by-three rectangle, a door on the west edge, a one-unit border, and a required north-edge latchment, the cycle runs as follows: the module is encoded to canonical text; the text is parsed by the LL(1) parser and the parse tree traversed to reconstruct an internal data structure identical to the original; and the structure is re-encoded under the canonical orthography to text that matches the original token for token. The demonstration is not specific to the example: deterministic encoding, unambiguous LL(1) parsing, and the injective canonical normalisation of INV-P-03 together fix one form per configuration and one configuration per form, which guarantees round-trip fidelity for every well-formed document.

7.24 Requirements traceability

The traceability matrix connects the ninety-eight frozen requirements to grammar productions, semantic definitions, and verification results. Of the ninety-eight, eighty are satisfied — the formal core directly meets them; eighteen are checkable — the core supplies the representational mechanism and full satisfaction awaits applied-grammar instantiation or a verification task on the twenty-five baseline entries; and none is unsatisfied, every requirement having a documented satisfaction pathway. The priority breakdown is as follows.

The two checkable P1 requirements — the applied-grammar plane-assignment table and validation coverage over the twenty-five baseline entries — are applied-grammar responsibilities discharged in the demonstration of Chapter 10. The matrix confirms that the design is complete with respect to its requirements specification: every P1 requirement has a concrete realisation in the grammar or its semantic rules, and the eighteen checkable requirements mark the boundary between the formal core’s responsibilities and the applied grammar’s.

7.25 Five demonstrated properties

The seven claims discharge Proposition 3 and the local component of Proposition 5 through five demonstrated properties, each a substrate-level result audited by an evidence object. Replay determinism: a canonical RecPol expression re-evaluated under the sealed grammar yields a byte-identical re-serialisation and a field-identical world-model state, because the closed token vocabulary, the LL(1) parser, and the canonical orthography together make the encode–decode pipeline a pure function over canonical expressions; the evidence record reports twenty-two of twenty-two deterministic checks passing, with no divergence between runs.²³ Invariant preservation across module boundaries: the twelve active inter-module boundary pairs of Chapter 6, tested under a contained-change and a propagating-change regime, yield twenty-four of twenty-four passing, with propagation occurring only through the interface type active for each pair.²⁴ Goodman compliance: both the symbol gate and the full-grammar gate record 5/5 PASS, qualified by the self-referentiality declaration of Section 7.12. Round-trip fidelity: the encode–decode–encode cycle preserves information for every well-formed document, on the structural basis of INV-P-03 and the empirical basis of the round-trip register. Local-to-global verification scope reduction: under the modular regime a change at one boundary pair triggers verification only on that pair’s active interface contracts, where a monolithic regime would trigger verification on every contract of every pair sharing a module endpoint — the verification economy that the modular architecture buys. The five properties jointly establish the Proposition 3 evidence base; Claim C7-1 is logically prior to them, since without machine-operable representation the executable mechanism cannot be invoked, and Claim C7-2 attaches to Proposition 5 by establishing that the two-layer architecture preserves separation of concerns under extensibility.

7.26 Contributions

The notation’s contribution to the thesis is best stated not as a list of separate achievements but as one evidence-bearing instantiation of the single architectural claim the thesis makes: it is the notation under which the governed-kernel modularity engine becomes machine-inspectable, parseable, and transformation-safe — the form in which the architecture’s commitments can be verified rather than asserted. That single role is discharged through several facets, each developed in the preceding sections, and the facets are worth naming precisely because each carries a distinct part of the verification burden, not because each is an independent thesis-level result.

The formal core, RecPol, develops a domain-agnostic, governance-capable formal language for rectangular polyominoes on a discrete integer grid with verified Goodman notational compliance. It stands in a clear relation to its precursors: the polyomino tradition — Golomb’s combinatorics of tiling, packing, and counting; Redelmeier’s enumeration algorithm; the group-action counting that supports free-polyomino enumeration — develops the polyomino as a combinatorial object, and the shape-grammar tradition initiated by Stiny and Gips develops a generative apparatus for spatial composition under rules.²⁵ What RecPol adds to that lineage is compliance as a first-class language-design criterion: its syntax encodes composition hierarchies, its semantics enforce stratification and verification ordering, and its canonical orthography guarantees round-trip fidelity, so that the symbol system itself — not a downstream pipeline stage layered over it — carries the governance discipline. The applied layer, PlaniSyn, develops a compliance-checkable text notation for accessible-dwelling spatial arrangement, grounded in the formal substrate and validated against the corpus-derived module system, encoding both geometry and dwelling-domain semantics in a single notation that meets the representational-substrate requirements of Chapter 3. The two-layer architecture develops a machine-checkable wrapping functor binding the applied grammar to a frozen formal core, so that domain-specific layers extend the core without modifying its productions and without re-running its notational and parsing certifications; the requirements-traced development process and the Goodman-compliance gate are the evidence discipline through which these facets are made auditable.

Two of the facets restate as design-science technological rules, which is the form in which they are examiner-auditable under the prescriptive-knowledge obligation of design science research. The first: to express compliance-checkable spatial composition in a domain that demands machine-verifiable governance, use a polyomino formalism extended with reserved extension-point tokens binding to a frozen formal core through a wrapping functor, because that combination satisfies Goodman’s five notational criteria at both the symbol and the full-grammar levels and supplies the determinacy that executable transformation logic requires. The second: to extend a sealed formal language with domain-specific vocabulary without re-running its notational and parsing certifications, introduce a fixed inventory of reserved extension-point tokens consumed only by the applied layer together with a deterministic desugaring map from applied-grammar constructs to formal-core entity blocks, because the reservation discipline leaves the core grammar’s decision sets unmodified and the desugaring map’s identity- and composition-preservation guarantee semantic equivalence with the governed kernel by construction. Each names a context, a mechanism, and a justification, and each generalises beyond the dwelling domain to any sealed grammar whose extension introduces only fresh terminals and a structure-preserving desugaring map.

7.27 Limitations

Six limitations bound the chapter’s claims. First, PlaniSyn is the only applied grammar constructed over RecPol here; the extensibility claim is supported by the formal architecture but not yet by a demonstrated second applied grammar, and constructing one — for hospital-ward or warehouse layout — would supply direct empirical support, which we identify as future work. Second, no working parser is implemented; the contribution is the notation design and its formal properties, and a parser is an engineering task that would validate implementability without affecting the formal properties. Third, the validation is internal — requirements traceability, Goodman compliance, and round-trip fidelity within the notation’s own terms — and does not demonstrate that the notation produces valid representations of real dwelling plans under realistic design conditions; that external validation is the responsibility of Chapter 10, which tests the notation against the Australian floor-plan corpus and through complex SDA case studies. Fourth, constraint completeness is bounded by the governed kernel’s thirty-two hard and eleven soft constraints; constraints arising from design practice but absent from the SDA corpus would require extending the constraint vocabulary through the governed mechanism, which this thesis does not exercise. Fifth, Goodman compliance is verified at the formal-core grammar level, and a full re-run of the gate over the composed RecPol-plus-PlaniSyn system is deferred; a structural argument that the 5/5 PASS lifts to the composition is available now and is set out below. Sixth, the generative-constraint vocabulary may be insufficient for advanced generative methods requiring richer parametric descriptions, and extending it through the extension mechanism is possible but unexplored.

The fifth limitation deserves its argument. On the syntactic side, three criteria — syntactic disjointness, syntactic finite differentiation, and the disjoint-decision-set property underwriting the LL(1) determinacy — are properties of the union of the formal-core and applied-grammar token sets. Because PlaniSyn introduces its syntax only through the six reserved extension-point tokens, whose decision sets are disjoint from every formal-core production’s by construction, and because the applied grammar may not redefine any core production, the applied grammar extends the union of decision sets without intersecting the core’s existing ones, preserving the pairwise-disjoint condition at all eleven decision points already verified for the core; the applied grammar therefore inherits syntactic disjointness and finite differentiation. On the semantic side, the remaining criteria are properties of the compliance-class assignment from token sequences to denotations. Because Contract SC-5 requires every PlaniSyn construct to denote what its desugared formal-core image denotes, and because the desugaring map is deterministic, total, and validity-preserving, every PlaniSyn semantic assertion is derivable from formal-core operations whose semantic determinacy is already certified; no PlaniSyn token can acquire a second compliance class without rendering the applied grammar non-conformant. The semantic criteria therefore lift through the wrapping functor by structural argument: any divergence would, by construction, be a non-conformant applied grammar rather than a Goodman-non-compliant one. The conclusion is that the 5/5 PASS obtained at the formal-core level lifts structurally to the composed system, under the explicit qualification that this is a structural argument grounded in the extensibility-contract clauses, not an empirical re-run of the gate over the composed grammar — a qualification that matters, because an adversarial examiner is entitled to demand the re-run, and the future-work entry above makes that re-run an explicit deferred deliverable.

7.28 Handoff contracts to Chapter 9

The notation’s handoff to Chapter 9 is governed by six formal contracts, mirroring Chapter 6’s handoff to this chapter. HC-7A (notation grammar transmission) transmits the complete two-layer system as input to the procedural generation pipeline; Chapter 9 may consume notation instances but may not modify the grammar, and a required capability the grammar lacks is flagged as a Chapter 7 specification gap. HC-7B (symbol constraints and representation rules) transmits the canonical orthography, the tokenisation rules, and the canonical normalisation invariant; non-canonical output is a generation defect, not a notation defect. HC-7C (encoding/parsing protocol with round-trip fidelity) transmits the eight-step pipeline, the LL(1) parsing procedure, and the round-trip guarantee, on which Chapter 9 may rely without independent verification. HC-7D (extensibility contract) transmits the wrapping-functor specification and the five semantic contracts; any generation-metadata tokens Chapter 9 requires must be introduced through the extension-point mechanism under Contract SC-2. HC-7E (P3 evidence objects) transmits the two evidence objects — the replay-determinism record binding evaluation measure EM-4W-02 and the invariant-preservation record binding EM-09-02 — which Chapter 9 may consume in its verification harness but may not modify without reopening the relevant evaluation stage. HC-7F (P5 evaluation inputs) transmits the requirements traceability matrix and the two Goodman gate results as preconditions for any P5 evaluation Chapter 9 conducts; a checkable requirement may not be relaxed to unsatisfied through a generation-pipeline simplification without reopening Chapter 7’s specification-defect register. The six contracts give the downstream chapter a single, audited intake point.

7.29 Forward to Chapter 9

The notation is now specified: a two-layer formal notation that renders the governed-kernel architecture machine-representable, parseable, and transformation-safe, in which every element of the module library — every primitive, relation, module type, constraint, and interface — is expressible in a notation that satisfies Goodman’s notational criteria and guarantees deterministic parsing and round-trip fidelity. The notation supplies the representational substrate; Chapter 9 receives it and develops the procedural generation pipeline that converts notation instances into documentation-ready dwelling plans, carrying the artefact suite a further step from corpus-derived specification toward machine-generated, governance-preserving housing documentation.

Navigation: ← 7.13 PlaniSyn: The Applied Layer | ↑ Chapter 7 | Chapter 8: Evidence from a Census of Australian Floor Plans →