Axiom DSL 语法规范三明治结构版概述本 DSL 是对axioms.md中公理书写语法的形式化提炼与规范定义。核心变革是废除行内元数据尾缀强制采用---meta三明治结构彻底消除|的语法歧义。设计原则分离关注点公式体Formula_body只含纯逻辑公式元数据由独立---meta块承载消除歧义公式体内的|只表示逻辑合取/析取/集合构造---meta是唯一的元数据边界标记编译友好解析器只需识别---meta之前的 Formula_body纯逻辑公式元数据由独立解析器处理双向追溯元数据既可嵌入公理声明内行内文档也可在独立元数据仓储中维护1. 行类型前缀前缀含义适用对象##元文档声明顶层文档描述//注释 / 章节标题自然语言段落、章节分组无前缀公理声明单行公式核心公理公式!公理定义块多行/代码块MetaEvolution、代码块公式[AX]/[AX-CORE]等公理类别标记公理声明行首%配置参数配置参数条目#推论 [TH]推论声明 推导缺陷记录缺陷修复上下文---分隔线节与节之间[Type]类型声明类型基底中的原始类型$符号约定符号约定表条目2. 行结构2.1 公理声明无前缀 / [TAG] 前缀— 三明治结构[TAG] 公理名: 纯逻辑公式体Formula_body ---meta key1 val1 key2 val2, val3 key3 type: predicate_expression ---[TAG]公理层级标记可选。如[AX]、[AX-CORE]、[BAX]、[BAX-X]、[AX-FRAME]、[AX-META]公理名公理标识符如IDI-Identity、StateSnapshot纯逻辑公式体Formula_body用|分隔的多个逻辑子句|在此只表示逻辑合取/析取/集合构造无元数据语义---meta元数据块开始标记独占一行key value元数据条目每行一个键值对格式---元数据块结束标记独占一行示例[AX] StateSnapshot: ∀op∈Ops,∀s∈Snap:op.readsFrom(s)→deterministic ---meta view D src Discrete-AtomicStep ---公式体内的|用法公式体内|仅用于逻辑合取/析取子句分隔集合构造多条件枚举[BAX-IDI] IDI-Identity: ∀(x:Entity),(obs:OBSERVER):x≡_obsx | ∀(x:Entity),(y:Entity),(obs:OBSERVER):(x≡_obsy)↔∀P∈Obs(obs)(P(x)↔P(y)) | Obs(obs)由L0注入而非递归自省 | (x≡_obs₁y)∧(x≢_obs₂y)→ep_gap(obs₁,obs₂) | Obs(obs)∌λP.P∈Obs(obs) ---meta view IDI irr logical src primitive sem conceptidentity, bindingobserver, impepistemic_gap dr 绝对莱布尼兹律在分布式系统中失效→引入Observer参数解决拜占庭分歧;Obs自指约束阻止罗素悖论 ---可省略的---meta块若某公理无需元数据可完全省略---meta块[AX] 纯公式公理: ∀x:P(x)解析器仍将其识别为合法公理声明元数据视为空。2.2 公理定义块!前缀— 三明治结构用于多行公式、代码块内容、附加约束! 公理名: 子句1 | 子句2 | 子句3 ---meta key1 val1 key2 val2 ---!后的第一行是子句集合续行使用|前缀公式体结束后使用---meta块若无需元数据可省略---meta块示例! CompensatePhase(阶段3-补偿): TryPhase超时后进入补偿路径(回滚恢复,非原子) | completed(sync)↔Commited(sync)∨Compensated(sync) | 路径1(正常→Commit):Try→Commit→Completed(Commited) | 路径2(超时→补偿):Try→Timeout→Compensate→Completed(Compensated) | 路径3(崩溃恢复):obs₁.recovered→使用本地持久化快照→重入Try ---meta irr relational view IDI src LogicalClock, CausalCone ---2.3 配置参数%前缀% 参数名 类型:默认值 | sem:说明 | authority:{权限}配置参数行较短允许行内尾缀格式因配置参数无复杂公式体不存在|歧义问题。示例% MAX_FAIL int:3 | sem:最大CF,达到后触发TM | authority:config(部署注入),runtime(需admin验证)2.4 推论#前缀# TH-编号: 结论公式 | src:{源公理列表} | pf:{推导步骤}推论也允许行内尾缀格式因推论体通常为单个结论公式|歧义不明显。示例# TH-5: ∀op₁,op₂:op₁.domain≠op₂.domain→needsSync(op₁,op₂)↔¬(op₁∥op₂) | src:{IDI-Interaction,Coupling-ObservationCollapse,SyncProtocolTriple.CommitPhase}2.5 设计理由 — 已废弃内联至---meta块的dr键设计理由不再使用~前缀声明而是写入对应公理的---meta块中的dr键。---meta dr 设计理由压缩文本 ---2.6 缺陷记录前缀 缺陷ID: affected:{受影响公理} | symptom:{症状} | root:{根因} | fix:{修复方式}示例 Defect-1: affected:{SyncProtocolTriple} | symptom:CommitPhase无限回归 | root:原子性定义未分层 | fix:原子性仅限定在Commited子集2.7 类型声明[Type]前缀[Type] 类型名 含义 | domain:{论域约束}示例[Type] Entity 可指称实体 | domain:非空(至少包含OBSERVER)2.8 符号约定$前缀$ 符号 含义 | ref:{源公理}示例$ τ逻辑时钟标签(偏序) | ref:LogicalClock $ →happened-before偏序 | ref:LogicalClock3. 元数据键---meta块内可用键3.1 标准键列表键含义对应原标记值格式view三棱镜视角^^PERSPECTIVEIDI,C,D等src基底来源^^SRCAxiomA, AxiomBirr不可再抽象标注^^IRRlogical/informational/topological/relational/structuralsem语义结构化标签^^SEMkeyval, keyval, ...enf强制执行机制^^ENFORCE类型: 具体约束cfg配置参数引用^^CONFIGParamName1, ParamName2dr设计理由一行^^DR简短中文或英文dep废弃声明^^DEPRECATEDreplaced-by(新公理名)authority参数修改权限新增config/adminversion参数版本化绑定新增τ3.2 sem 值的结构化格式sem使用逗号分隔的键值对预定义子键sem 子键含义concept核心概念binding绑定对象imp主要推论/蕴含role在体系中的角色source来源说明rationale形式化理由3.3 enf 值的格式enf 类型: 谓词类型为runtime_invariant运行时不变式断言codegen_constraint代码生成约束inference_rule推理规则specification形式规范声明示例---meta enf runtime_invariant: ∀op∈MetaRound, op.target∉{BAX-IDI,BAX-TIME,BAX-C,BAX-D,SyncProtocolTriple} ---3.4 组合示例[AX] SampleAxiom: ∀x:P(x)∧Q(x) ---meta view IDI, D src IDI-Identity, Discrete-AtomicStep enf runtime_invariant: 每次决策后验证一致性 sem concept完成, role状态转移条件 ---4. 行内压缩规则4.1 逻辑符号缩写原扩展名DSL 缩写说明consecutive_failuresCF仅在公理公式内部上下文明确时使用consecutive_partialsCP同上quality_decline_countQDC同上iteration_countIC同上best_resultBR同上Obs_capabilities(obs)Obs(obs)观察者能力集epistemic_gapep_gap认知差距terminate_success/meltdown/overflowTS/TM/TO终止决策类型4.2 变量类型标注推荐使用完整形式∀(x:Entity)以避免歧义。4.3 中文注释压行代码块中的自然语言中文注释压缩为单行// DSL // 自指约束:Obs(obs)∌λP.P∈Obs(obs);元层级锚定在L0硬核5. 文法EBNF 简化版Document { Section | Comment | Separator } Section ## MetaDoc | SectionBlock SectionBlock AxiomDef | MultiLineBlock | ConfigDef | TheoremDef | DefectRecord | TypeDecl | SymbolDef AxiomDef [ Tag ] Name : FormulaBody NL ---meta NL { MetaLine } --- MultiLineBlock ! Name : Line { | Line } [ NL ---meta NL { MetaLine } --- ] ConfigDef % Name Type : Value { | SuffixEntry } TheoremDef # Name : Formula | src: { NameList } [ | pf: Steps ] DefectRecord DefectID : KeyValPairs TypeDecl [Type] Name Description [ | domain: Constraint ] SymbolDef $ Symbol Meaning [ | ref: Source ] FormulaBody Formula { | Formula } (* | 仅表示逻辑合取/析取/集合构造 *) Formula LogicalExpression MetaLine Key \ MetaValue \ MetaValue TextContent (* 键值的自由文本内容 *) SuffixEntry Key : SuffixValue SuffixValue { NameList } | TagList | ConceptPairs | EnforceExpr | AuthorityExpr | VersionExpr NameList Name { , Name } TagList Tag { , Tag } ConceptPairs ConceptPair { , ConceptPair } ConceptPair Key Value EnforceExpr Type ( Predicate ) AuthorityExpr config | admin | config , admin VersionExpr LogicalClockRef LogicalClockRef τ | τ_number Level L0 | L0.5 | L1 | L2 | L3 | D | C6. 转换规则总结旧版 → 三明治结构原结构旧版行内尾缀三明治结构等价[TAG] Name: 公式 | view:{X}[TAG] Name: 公式---metaview X---[TAG] Name: 公式 | sem:keyval[TAG] Name: 公式---metasem keyval---| enf:类型(谓词)---metaenf 类型: 谓词---| irr:类型---metairr 类型---| dr:文本---metadr 文本---~ 公理名: 理由对应公理---meta块中的dr键多行块!内的| irr:temporal | sem:...多行块后接---meta块承接^^PERSPECTIVE / ^^SRC / ^^IRR / ^^SEM / ^^ENFORCE / ^^DR / ^^CONFIG全部映射为---meta块内的对应键7. 公理分层编译策略公理到代码的编译映射、层级实现机制详见 spec.md §1。层级定义与不可变性约束由 axioms.md:[AX-CORE] AxiomHierarchyStructure声明代码生成策略层级映射表、编译流程、代码示例归入 spec.md §1。附录 A旧版语法兼容性说明本规范 v2.0三明治结构版与 v1.0行内尾缀版不完全兼容。兼容维度说明旧版解析器无法解析三明治结构不能识别---meta块新版解析器可识别旧版行内尾缀并发出弃用警告deprecation_warning自动迁移可使用迁移脚本将行内尾缀转换为---meta块%配置行保持行内尾缀格式不变因无 #推论行保持行内尾缀格式不变因推论体通常为单个公式建议所有新编公理强制使用三明治结构存量公理axioms.md迁移截止至下一大版本发布前。
Axiom DSL 语法规范三明治结构版概述本 DSL 是对axioms.md中公理书写语法的形式化提炼与规范定义。核心变革是废除行内元数据尾缀强制采用---meta三明治结构彻底消除|的语法歧义。设计原则分离关注点公式体Formula_body只含纯逻辑公式元数据由独立---meta块承载消除歧义公式体内的|只表示逻辑合取/析取/集合构造---meta是唯一的元数据边界标记编译友好解析器只需识别---meta之前的 Formula_body纯逻辑公式元数据由独立解析器处理双向追溯元数据既可嵌入公理声明内行内文档也可在独立元数据仓储中维护1. 行类型前缀前缀含义适用对象##元文档声明顶层文档描述//注释 / 章节标题自然语言段落、章节分组无前缀公理声明单行公式核心公理公式!公理定义块多行/代码块MetaEvolution、代码块公式[AX]/[AX-CORE]等公理类别标记公理声明行首%配置参数配置参数条目#推论 [TH]推论声明 推导缺陷记录缺陷修复上下文---分隔线节与节之间[Type]类型声明类型基底中的原始类型$符号约定符号约定表条目2. 行结构2.1 公理声明无前缀 / [TAG] 前缀— 三明治结构[TAG] 公理名: 纯逻辑公式体Formula_body ---meta key1 val1 key2 val2, val3 key3 type: predicate_expression ---[TAG]公理层级标记可选。如[AX]、[AX-CORE]、[BAX]、[BAX-X]、[AX-FRAME]、[AX-META]公理名公理标识符如IDI-Identity、StateSnapshot纯逻辑公式体Formula_body用|分隔的多个逻辑子句|在此只表示逻辑合取/析取/集合构造无元数据语义---meta元数据块开始标记独占一行key value元数据条目每行一个键值对格式---元数据块结束标记独占一行示例[AX] StateSnapshot: ∀op∈Ops,∀s∈Snap:op.readsFrom(s)→deterministic ---meta view D src Discrete-AtomicStep ---公式体内的|用法公式体内|仅用于逻辑合取/析取子句分隔集合构造多条件枚举[BAX-IDI] IDI-Identity: ∀(x:Entity),(obs:OBSERVER):x≡_obsx | ∀(x:Entity),(y:Entity),(obs:OBSERVER):(x≡_obsy)↔∀P∈Obs(obs)(P(x)↔P(y)) | Obs(obs)由L0注入而非递归自省 | (x≡_obs₁y)∧(x≢_obs₂y)→ep_gap(obs₁,obs₂) | Obs(obs)∌λP.P∈Obs(obs) ---meta view IDI irr logical src primitive sem conceptidentity, bindingobserver, impepistemic_gap dr 绝对莱布尼兹律在分布式系统中失效→引入Observer参数解决拜占庭分歧;Obs自指约束阻止罗素悖论 ---可省略的---meta块若某公理无需元数据可完全省略---meta块[AX] 纯公式公理: ∀x:P(x)解析器仍将其识别为合法公理声明元数据视为空。2.2 公理定义块!前缀— 三明治结构用于多行公式、代码块内容、附加约束! 公理名: 子句1 | 子句2 | 子句3 ---meta key1 val1 key2 val2 ---!后的第一行是子句集合续行使用|前缀公式体结束后使用---meta块若无需元数据可省略---meta块示例! CompensatePhase(阶段3-补偿): TryPhase超时后进入补偿路径(回滚恢复,非原子) | completed(sync)↔Commited(sync)∨Compensated(sync) | 路径1(正常→Commit):Try→Commit→Completed(Commited) | 路径2(超时→补偿):Try→Timeout→Compensate→Completed(Compensated) | 路径3(崩溃恢复):obs₁.recovered→使用本地持久化快照→重入Try ---meta irr relational view IDI src LogicalClock, CausalCone ---2.3 配置参数%前缀% 参数名 类型:默认值 | sem:说明 | authority:{权限}配置参数行较短允许行内尾缀格式因配置参数无复杂公式体不存在|歧义问题。示例% MAX_FAIL int:3 | sem:最大CF,达到后触发TM | authority:config(部署注入),runtime(需admin验证)2.4 推论#前缀# TH-编号: 结论公式 | src:{源公理列表} | pf:{推导步骤}推论也允许行内尾缀格式因推论体通常为单个结论公式|歧义不明显。示例# TH-5: ∀op₁,op₂:op₁.domain≠op₂.domain→needsSync(op₁,op₂)↔¬(op₁∥op₂) | src:{IDI-Interaction,Coupling-ObservationCollapse,SyncProtocolTriple.CommitPhase}2.5 设计理由 — 已废弃内联至---meta块的dr键设计理由不再使用~前缀声明而是写入对应公理的---meta块中的dr键。---meta dr 设计理由压缩文本 ---2.6 缺陷记录前缀 缺陷ID: affected:{受影响公理} | symptom:{症状} | root:{根因} | fix:{修复方式}示例 Defect-1: affected:{SyncProtocolTriple} | symptom:CommitPhase无限回归 | root:原子性定义未分层 | fix:原子性仅限定在Commited子集2.7 类型声明[Type]前缀[Type] 类型名 含义 | domain:{论域约束}示例[Type] Entity 可指称实体 | domain:非空(至少包含OBSERVER)2.8 符号约定$前缀$ 符号 含义 | ref:{源公理}示例$ τ逻辑时钟标签(偏序) | ref:LogicalClock $ →happened-before偏序 | ref:LogicalClock3. 元数据键---meta块内可用键3.1 标准键列表键含义对应原标记值格式view三棱镜视角^^PERSPECTIVEIDI,C,D等src基底来源^^SRCAxiomA, AxiomBirr不可再抽象标注^^IRRlogical/informational/topological/relational/structuralsem语义结构化标签^^SEMkeyval, keyval, ...enf强制执行机制^^ENFORCE类型: 具体约束cfg配置参数引用^^CONFIGParamName1, ParamName2dr设计理由一行^^DR简短中文或英文dep废弃声明^^DEPRECATEDreplaced-by(新公理名)authority参数修改权限新增config/adminversion参数版本化绑定新增τ3.2 sem 值的结构化格式sem使用逗号分隔的键值对预定义子键sem 子键含义concept核心概念binding绑定对象imp主要推论/蕴含role在体系中的角色source来源说明rationale形式化理由3.3 enf 值的格式enf 类型: 谓词类型为runtime_invariant运行时不变式断言codegen_constraint代码生成约束inference_rule推理规则specification形式规范声明示例---meta enf runtime_invariant: ∀op∈MetaRound, op.target∉{BAX-IDI,BAX-TIME,BAX-C,BAX-D,SyncProtocolTriple} ---3.4 组合示例[AX] SampleAxiom: ∀x:P(x)∧Q(x) ---meta view IDI, D src IDI-Identity, Discrete-AtomicStep enf runtime_invariant: 每次决策后验证一致性 sem concept完成, role状态转移条件 ---4. 行内压缩规则4.1 逻辑符号缩写原扩展名DSL 缩写说明consecutive_failuresCF仅在公理公式内部上下文明确时使用consecutive_partialsCP同上quality_decline_countQDC同上iteration_countIC同上best_resultBR同上Obs_capabilities(obs)Obs(obs)观察者能力集epistemic_gapep_gap认知差距terminate_success/meltdown/overflowTS/TM/TO终止决策类型4.2 变量类型标注推荐使用完整形式∀(x:Entity)以避免歧义。4.3 中文注释压行代码块中的自然语言中文注释压缩为单行// DSL // 自指约束:Obs(obs)∌λP.P∈Obs(obs);元层级锚定在L0硬核5. 文法EBNF 简化版Document { Section | Comment | Separator } Section ## MetaDoc | SectionBlock SectionBlock AxiomDef | MultiLineBlock | ConfigDef | TheoremDef | DefectRecord | TypeDecl | SymbolDef AxiomDef [ Tag ] Name : FormulaBody NL ---meta NL { MetaLine } --- MultiLineBlock ! Name : Line { | Line } [ NL ---meta NL { MetaLine } --- ] ConfigDef % Name Type : Value { | SuffixEntry } TheoremDef # Name : Formula | src: { NameList } [ | pf: Steps ] DefectRecord DefectID : KeyValPairs TypeDecl [Type] Name Description [ | domain: Constraint ] SymbolDef $ Symbol Meaning [ | ref: Source ] FormulaBody Formula { | Formula } (* | 仅表示逻辑合取/析取/集合构造 *) Formula LogicalExpression MetaLine Key \ MetaValue \ MetaValue TextContent (* 键值的自由文本内容 *) SuffixEntry Key : SuffixValue SuffixValue { NameList } | TagList | ConceptPairs | EnforceExpr | AuthorityExpr | VersionExpr NameList Name { , Name } TagList Tag { , Tag } ConceptPairs ConceptPair { , ConceptPair } ConceptPair Key Value EnforceExpr Type ( Predicate ) AuthorityExpr config | admin | config , admin VersionExpr LogicalClockRef LogicalClockRef τ | τ_number Level L0 | L0.5 | L1 | L2 | L3 | D | C6. 转换规则总结旧版 → 三明治结构原结构旧版行内尾缀三明治结构等价[TAG] Name: 公式 | view:{X}[TAG] Name: 公式---metaview X---[TAG] Name: 公式 | sem:keyval[TAG] Name: 公式---metasem keyval---| enf:类型(谓词)---metaenf 类型: 谓词---| irr:类型---metairr 类型---| dr:文本---metadr 文本---~ 公理名: 理由对应公理---meta块中的dr键多行块!内的| irr:temporal | sem:...多行块后接---meta块承接^^PERSPECTIVE / ^^SRC / ^^IRR / ^^SEM / ^^ENFORCE / ^^DR / ^^CONFIG全部映射为---meta块内的对应键7. 公理分层编译策略公理到代码的编译映射、层级实现机制详见 spec.md §1。层级定义与不可变性约束由 axioms.md:[AX-CORE] AxiomHierarchyStructure声明代码生成策略层级映射表、编译流程、代码示例归入 spec.md §1。附录 A旧版语法兼容性说明本规范 v2.0三明治结构版与 v1.0行内尾缀版不完全兼容。兼容维度说明旧版解析器无法解析三明治结构不能识别---meta块新版解析器可识别旧版行内尾缀并发出弃用警告deprecation_warning自动迁移可使用迁移脚本将行内尾缀转换为---meta块%配置行保持行内尾缀格式不变因无 #推论行保持行内尾缀格式不变因推论体通常为单个公式建议所有新编公理强制使用三明治结构存量公理axioms.md迁移截止至下一大版本发布前。
)
