This paper constitutes a preliminary attempt at formal modeling of a top-level structural framework, aiming to propose a possible theoretical structure. The current model has not yet undergone verification of completeness, consistency, or adequacy. Its expressive power and categorical-semantic interpretation also remain to be rigorously examined.
The background of this work lies in the development of legal artificial intelligence and computational law. As these fields advance, the structuring, formalization, and computable representation of legal knowledge have become important issues. Formal modeling helps construct calculable legal structural models, providing a foundation for automated reasoning, rule verification, and the establishment of computational frameworks. The top-level design proposed in this paper is intended to offer an abstract structural direction for the subsequent development of such computational models.
This paper does not claim that the system presented constitutes a complete theoretical representation of civil law, but rather serves as an exploratory construction at the structural level.
I. SYNTAX
The syntactic layer defines only well-formed symbolic constructions and does not involve any semantic interpretation.
Sort (Type Identifiers)
$$ \text{Sort} ::= \text{Entity} \mid \text{Process} \mid \text{Event} \mid \text{State} \mid \text{Property} \mid \text{Relation} \mid s \otimes t \mid s \oplus t \mid \wp(s) $$
Fact (Type Family)
$$ \text{Fact} : \text{Sort} \to \mathsf{Type} $$
Intuitively, for each sort $s$, $\text{Fact}(s)$ denotes the collection of fact expressions of type $s$.
(** * legal_core.v Category-theoretic formalization of legal facts. Based on the legal_core specification (Syntax + Semantics). Structure: I. Sorts & Identifiers II. Fact type (objects of the category) III. Term constructors IV. Judgments (transitions, normative derivations) V. Paths & Path equivalence VI. Category structure ℒ VII. Worked examples *)
From Stdlib Require Import Lists.List. From Stdlib Require Import Relations.Relation_Definitions. From Stdlib Require Import Relations.Relations. Import ListNotations.
(** A tag that names a relation kind (e.g., "代理", "债"). *) Parameter RelTag : Type.
(* ================================================================= *) (** ** II. FACT — objects of the category ℒ *) (* ================================================================= *)
(** Fact(s) is the type of legal facts of sort [s]. This is an *inductive family* indexed by Sort.
Constructors mirror the typing rules in §II of the spec: - Six atomic constructors (one per sort) - ι_s : sort-embedding into Entity - rel : binary relation between two facts - has_attr : attribute attachment - evolve : recursive process construction *) Inductive Fact : Sort -> Type :=
(* §II Recursive process construction: evolve(A, B) : Fact(Process) *) | evolve : forall (s t : Sort), Fact s -> Fact t -> Fact SProcess.
(* ================================================================= *) (** ** III. TERMS — a flat universe for heterogeneous fact values *) (* ================================================================= *)
(** A [Term] is a sigma-type pairing a sort with a fact of that sort. This lets us write functions that work over all sorts uniformly. *) Definition Term : Type := { s : Sort & Fact s }.
(** Smart constructors (mirror the Term grammar). *) Definition term_entity (i : EntId) : Term := existT _ SEntity (fact_entity i). Definition term_process (i : ProcId) : Term := existT _ SProcess (fact_process i). Definition term_event (i : EventId) : Term := existT _ SEvent (fact_event i). Definition term_state (i : StateId) : Term := existT _ SState (fact_state i). Definition term_property (i : PropId) : Term := existT _ SProperty (fact_property i). Definition term_relation (i : RelId) : Term := existT _ SRelation (fact_relation i).
(* -- *) (** *** IV-a. Single-step transition Γ ⊢ A —e→ B *) (* -- *)
(** [Transition A e B] encodes the judgment A —e→ B where [e : Fact SEvent] is the triggering event. *) Inductive Transition : forall (s t : Sort), Fact s -> Fact SEvent -> Fact t -> Prop :=
(** §II Single-step rule: A : Fact(s), e : Fact(Event), B : Fact(t) ───────────────────────────────────────────── A —e→ B *) | step : forall (s t : Sort) (A : Fact s) (e : Fact SEvent) (B : Fact t), Transition s t A e B
(** §II Composition rule: A —e1→ B, B —e2→ C ───────────────────────────────────────────── A —e2∘e1→ C We represent the composite event as a fresh [Fact SEvent] produced by reification (see reify below). *) | compose_step : forall (s t u : Sort) (A : Fact s) (e1 : Fact SEvent) (B : Fact t) (e2 : Fact SEvent) (C : Fact u), Transition s t A e1 B -> Transition t u B e2 C -> Transition s u A e2 C. (* composite; event label simplified *)
(** [reify] turns a transition proof into a first-class event fact. In Coq we model this as an axiom (it extends the term language). *) Axiom reify : forall (s t : Sort) (A : Fact s) (e : Fact SEvent) (B : Fact t), Transition s t A e B -> Fact SEvent.
(* -- *) (** *** IV-c. Normative derivation Γ ⊢ A ⇒ B *) (* -- *)
(** [Norm A B] is the normative entailment judgment A ⇒ B. *) Parameter Valid : forall (s : Sort), Fact SEvent -> Prop.
Inductive Norm : forall (s t : Sort), Fact s -> Fact t -> Prop :=
(** §II Pure normative derivation: A : Fact(s), B : Fact(t) ─────────────────────────── A ⇒ B *) | norm_direct : forall (s t : Sort) (A : Fact s) (B : Fact t), Norm s t A B
(** §II Normative bridging (via valid event): A —e→ B, Valid(e) ─────────────────────────────────────── A ⇒ B *) | norm_bridge : forall (s t : Sort) (A : Fact s) (e : Fact SEvent) (B : Fact t), Transition s t A e B -> Valid SEvent e -> Norm s t A B.
(** A path is a sequence of transitions from A to B of any sorts. We represent a path as a list of composable transition witnesses. *) Inductive Path : forall (s t : Sort), Fact s -> Fact t -> Type := | path_id : forall (s : Sort) (A : Fact s), Path s s A A | path_step : forall (s t u : Sort) (A : Fact s) (e : Fact SEvent) (B : Fact t) (C : Fact u), Transition s t A e B -> Path t u B C -> Path s u A C.
(** Path equivalence: two paths between the same endpoints are ≈. Axiomatised as a setoid equality (reflexive, symmetric, transitive). *) Parameter path_equiv : forall (s t : Sort) (A : Fact s) (B : Fact t), Path s t A B -> Path s t A B -> Prop.
Axiom path_equiv_refl : forall s t A B (p : Path s t A B), p ≈ p. Axiom path_equiv_sym : forall s t A B (p q : Path s t A B), p ≈ q -> q ≈ p. Axiom path_equiv_trans : forall s t A B (p q r : Path s t A B), p ≈ q -> q ≈ r -> p ≈ r.
(** Concatenation of paths (like [app] for lists). *) Fixpoint path_compose {s t u : Sort} {A : Fact s} {B : Fact t} {C : Fact u} (p : Path s t A B) (q : Path t u B C) : Path s u A C := match p with | path_id _ _ => q | path_step _ _ _ _ e _ _ tr rest => path_step _ _ _ _ e _ C tr (path_compose rest q) end.
(** Left identity: id ∘ p ≈ p *) Lemma path_id_left : forall (s t : Sort) (A : Fact s) (B : Fact t) (p : Path s t A B), path_compose (path_id s A) p ≈ p. Proof. intros. simpl. apply path_equiv_refl. Qed.
(** Right identity: p ∘ id ≈ p *) Lemma path_id_right : forall (s t : Sort) (A : Fact s) (B : Fact t) (p : Path s t A B), path_compose p (path_id t B) ≈ p. Proof. intros s t A B p. induction p as [| s' t' u' A' e B' C' tr rest IH]. - apply path_equiv_refl. - simpl. (* path_step ... (path_compose rest id_B) ≈ path_step ... rest *) (* This relies on congruence over path_equiv; axiomatised below *) admit. Admitted.
(** Associativity: (p ∘ q) ∘ r ≈ p ∘ (q ∘ r) *) Lemma path_assoc : forall (s t u v : Sort) (A : Fact s) (B : Fact t) (C : Fact u) (D : Fact v) (p : Path s t A B) (q : Path t u B C) (r : Path u v C D), path_compose (path_compose p q) r ≈ path_compose p (path_compose q r). Proof. intros. induction p as [| s' t' u' A' e B' C' tr rest IH]. - simpl. apply path_equiv_refl. - simpl. admit. Admitted.
Theorem left_identity : forall (X Y : Ob) (f : Hom X Y), path_equiv _ _ _ _ (compose (id X) f) f. Proof. intros. apply path_id_left. Qed.
Theorem right_identity : forall (X Y : Ob) (f : Hom X Y), path_equiv _ _ _ _ (compose f (id Y)) f. Proof. intros. apply path_id_right. Qed.
Theorem associativity : forall (X Y Z W : Ob) (f : Hom X Y) (g : Hom Y Z) (h : Hom Z W), path_equiv _ _ _ _ (compose (compose f g) h) (compose f (compose g h)). Proof. intros. apply path_assoc. Qed.
End LegalCategory.
(* ================================================================= *) (** ** VII. WORKED EXAMPLES *) (* ================================================================= *)
(** Reify the transition back to an event object. *) Definition ownership_event : Fact SEvent := reify SEntity SState RightHolder ContractSigned OwnershipEstablished acquire_ownership.
(** A process evolving from entity to state. *) Definition AcquisitionProcess : Fact SProcess := evolve SEntity SState RightHolder OwnershipEstablished.
(** Print the types of key definitions for verification. *) Check acquire_ownership. Check acquisition_path. Check composed_transition. Check valid_contract_implies_ownership. Check LegalCategory.compose.
(** Summary of the category ℒ :
Ob(ℒ) = Fact(s) for s ∈ {Entity, Process, Event, State, Property, Relation}
Hom(A, B) = Path from A to B (sequences of single-step Transition witnesses)
id_A = path_id _ A (zero-length path) g ∘ f = path_compose f g (concatenation)
Axioms: left/right identity, associativity (up to path_equiv ≈)
Additional structure: - Norm A B : normative entailment (A ⇒ B) - reify e : transition → Event fact (event reification) - evolve A B : (A, B) → Process fact (process construction) - rel r A B : (A, B) → Relation fact - has_attr A P : (A, P) → Relation fact (attribute attachment) - iota_s A : Fact(s) → Fact(Entity) (sort embedding) *)