NS-L6 Standard - Appendix B — Formal Semantics

SPECIFICATION · VERSION 1.1

NS-L6 v1.1 — Human–LLM Responsibility Framework

The authoritative normative specification of the Human–LLM Responsibility Framework.
This release defines the structural, procedural, and epistemic invariants required to maintain deterministic responsibility boundaries.

Read Framework Read RFC Layer

NS-L6 Standard — v1.1

Status: FINAL — Normative Publication

Canonical Source:
GitHub Release — v1.1

Version 1.1 provides the first complete and formally validated public release of the NS-L6 Standard. It includes the core specification, supporting RFC, and a set of foundational normative appendices establishing semantics, proofs, and threat models.

Included Documents

Framework NS-L6 Framework v1.1
RFC NS-L6 RFC v1.1
Appendix A Formal Proofs (Public Extract)
Appendix B Formal Semantics / BNF
Appendix C Threat Model

NS-L6 Appendix B — Formal Semantics (BNF/EBNF)

B.1 Purpose (Informative)

This appendix defines the formal semantics of the NS-L6 Standard using Extended Backus–Naur Form (EBNF). The grammar provides the structural rules for responsibility mappings, state declarations, time indices, transitions, and compliance constructs.

B.2 Semantic Domains (Normative)

Layer        = L0 | L1 | L2 | L3 | L4 | L5 | L6 ;
State        = identifier ;
TimeIndex    = integer ;
Actor        = identifier ;
ResponsibilitySet = "∅" | "{" ResponsibilityItem ("," ResponsibilityItem)* "}" ;
ResponsibilityItem = identifier ;

B.3 Core Grammar Definitions (Normative)

B.3.1 Responsibility Mapping

ResponsibilityMapping =
    "R" "(" Actor "," Layer "," State "," TimeIndex ")" "→" ResponsibilitySet ;

Layers L0–L3 MUST have ∅ responsibility.
L4 MAY contain technical responsibilities.
L5–L6 MUST NOT be ∅.

B.3.2 Observability and Controllability Rules

Observability  = "Obs"  "(" Actor "," Layer ")" "=" ( "True" | "False" ) ;
Controllability = "Ctrl" "(" Actor "," Layer ")" "=" ( "True" | "False" ) ;

Mandatory consistency:

R(a, i, t) ≠ ∅ ⇔ Obs(a, i) = True AND Ctrl(a, i) = True ;

B.3.3 Layer Transition Semantics

Transition =
    Layer "." "T" "(" State "," TimeIndex ")" "=" State ;

Transitions MUST be non-invertible for all i < j.
Bidirectional transitions MUST NOT exist.

B.3.4 State Declarations

StateDeclaration =
    Layer "." "State" "(" TimeIndex ")" "=" State ;

B.3.5 Imperative Compliance Syntax

ComplianceCheck =
    "CHECK" ImperativeName ":" ( "PASS" | "FAIL" ) ;

All NI-1 … NI-14 MUST be PASS for NS-L6 compliance.

B.4 Meta-Constraints (Normative)

B.4.1 Non-Invertibility

NonInvertible =
    "NONINV" "(" Layer "," Layer ")" "=" "True" ;

Required for all (i, j) with i < j.

B.4.2 Time Locality

TimeLocality =
    Layer "." "Time" "=" "LocalIndex" ;

No global time index is permitted.

B.5 Extended Grammar (Informative)

LogicExpr =
      "NOT" LogicExpr
    | LogicExpr "AND" LogicExpr
    | LogicExpr "OR"  LogicExpr
    | "(" LogicExpr ")"
    | Predicate ;

Predicate =
      Observability
    | Controllability
    | ResponsibilityMapping ;

B.6 Validation Rules (Normative)

All syntactic rules in B.2–B.5 MUST hold.
No ResponsibilityMapping may violate invariants.
NonInvertible(i, j) = True MUST hold for all i < j.
All NI-* rules MUST be PASS.

B.7 End of Appendix B

This appendix concludes the formal semantic grammar of NS-L6 v1.1.