IndisputableMonolith.Loom.Readings

   1import IndisputableMonolith.Loom.Grammar
   2
   3/-!
   4# What a collection of local facts can see
   5
   6The claim the separation witness is for is a claim about a RIVAL, so the rival has to be
   7defined here rather than left in a Python script. Two readings of content, both of them
   8the honest shape of a relational message:
   9
  10* `groundBag`, a multiset of typed tuples over shared vocabulary. This is what an ingest
  11  contract carries: facts over declared keys, plus a count of which binders occurred. It
  12  has no place to put nesting, because a scope node exists only inside one claim and has
  13  no name the receiver already knows.
  14* `adjacencyBag`, strictly stronger, which also carries every parent to child label pair
  15  of the parse tree. This one is not really a bag, since carrying it means carrying
  16  anonymous per claim nodes, and it is defined anyway because a witness that only defeats
  17  the weaker rival should say so.
  18
  19`adjacencyBag` folds denial into the atom's label, which is the FAIR version: a reading
  20that dropped polarity would be beaten by a triviality. Since `Expr` is already in
  21negation normal form, that is all denial there is.
  22
  23Equality of readings is stated as `List.Perm`, which is exactly equality of the
  24multisets, and it is decidable, so each blindness claim in `Separation.lean` is checked by
  25the kernel rather than asserted.
  26
  27Both readings are functions of content alone: neither ever looks at a loop. That is what
  28makes the separation matter rather than being an argument about encodings. A carrier that
  29reads content this way cannot be repaired by a better encoder downstream, because the
  30distinction is already gone before anything is encoded.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Loom
  35
  36/-- A node's label: what a local reading of the parse tree can name. -/
  37inductive Label where
  38  | root : Label
  39  | atom (pred : Nat) (args : List Nat) (denied : Bool) : Label
  40  | conj : Label
  41  | quant (universal : Bool) (binder : Nat) : Label
  42deriving DecidableEq, Repr
  43
  44/-- An entry of the ground reading: a fact over shared vocabulary, or the occurrence of a
  45binder. Nothing here can express which binder a fact sits under. -/
  46inductive Ground where
  47  | fact (pred : Nat) (args : List Nat) (denied : Bool) : Ground
  48  | binder (universal : Bool) (name : Nat) : Ground
  49deriving DecidableEq, Repr
  50
  51def labelOf : Expr → Label
  52  | .atom p args d => .atom p args d
  53  | .conj _ _ => .conj
  54  | .quant u b _ => .quant u b
  55
  56/-- The ground reading: facts and binder occurrences, with no attachment between them. -/
  57def groundBag : Expr → List Ground
  58  | .atom p args d => [.fact p args d]
  59  | .conj a b => groundBag a ++ groundBag b
  60  | .quant u b body => .binder u b :: groundBag body
  61
  62/-- The labelled adjacency reading: every parent to child edge of the parse tree, with
  63the root edge included so the top node is not free. -/
  64def adjacencyEdges : Expr → List (Label × Label)
  65  | .atom _ _ _ => []
  66  | .conj a b =>
  67      (Label.conj, labelOf a) :: (Label.conj, labelOf b) ::
  68        (adjacencyEdges a ++ adjacencyEdges b)
  69  | .quant u b body =>
  70      (Label.quant u b, labelOf body) :: adjacencyEdges body
  71
  72def adjacencyBag (e : Expr) : List (Label × Label) :=
  73  (Label.root, labelOf e) :: adjacencyEdges e
  74
  75end Loom
  76end IndisputableMonolith
  77