ZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics
We propose ZX-Calculus (Knowledge Evolution Calculus), a conservative extension of Martin-Lof Dependent Type Theory (MLTT) integrating trace-indexed types, presheaf non-monotone semantics, and constructive AGM belief revision. A Coq mechanisation accompanies the paper (34 complete proofs; zero admits for the two central results). (I) Trace types. FinTrace(s0,sn) is an inductive family of typed execution traces. FinTrace and Star(Step) are isomorphic as path types but not judgementally equal; TraceElim exposes the event label e:Event explicitly, giving a more ergonomic interface for event-driven induction. We prove the Trace-Reachability Correspondence, Deterministic Replay, and a canonicity framework via reducibility candidates with a Transport Lemma (RC-elim deferred; all other Core results are Coq-verified). (II) Sheaf semantics. Trace-indexed propositions are contravariant sheaves over the free trace partial-order category Tf. A Separation Theorem (explicit countermodel) distinguishes proof-theoretic monotonicity from semantic non-monotonicity. The term model is an initial CwF (syntactic universal property, not classical completeness). (III) AGM belief revision. We give an explicit constructive partial meet contraction algorithm verified against (C1)-(C4). All eight AGM postulates (R1)-(R8) are theorems. Proofs of R7 and R8 use the Disjunctive Entrenchment Lemma, given a self-contained constructive derivation. (IV) Integration. B^AGM fails the sheaf composition law BP-comp for sequential revision (explicit countermodel, Coq-verified). We introduce Single-Step Revision Systems (SSRS), prove B^AGM is a valid SSRS (Coq-verified), and show this suffices for trace morphisms, retraction characterisation, and revision witnesses. The BP-comp failure reveals a fundamental tension between path-dependent belief revision and functor consistency, not previously identified.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Better Understanding, Understanding Better
"Any fool can know; the point is to understand." A well-known remark often attributed to Einstein captures a widely shared intuition: understanding is more than merely knowing. Yet epistemic logic has paid relatively lit…
An extension of process calculus for asynchronous communications between agents with epistemic states
It plays a central role in intelligent agent systems to model agent's epistemic state and its change. Asynchrony plays a key role in distributed systems, in which the messages transmitted may not be received instantly by…
Pricing formulae for derivatives in insurance using the Malliavin calculus
In this paper we provide a valuation formula for different classes of actuarial and financial contracts which depend on a general loss process, by using the Malliavin calculus. In analogy with the celebrated Black-Schole…
A Defeasible Calculus for Zetetic Agents
The study of defeasible reasoning unites epistemologists with those working in AI, in part, because both are interested in epistemic rationality. While it is traditionally thought to govern the formation and (with)holdin…
Common Knowledge of Abstract Groups
Epistemic logics typically talk about knowledge of individual agents or groups of explicitly listed agents. Often, however, one wishes to express knowledge of groups of agents specified by a given property, as in `it is …