GOI-unification

GOI.agda

module GOI where

open import Prelude
open import Data.Nat
open import Data.List renaming (_++_ to _++ₗ_)
open import Data.List.Correspondences.Binary.Prefix
open import Data.Fin.Inductive
open import Data.Vec.Inductive
open import Data.Vec.Inductive.Operations as Vec
open import Data.Star
open import Data.Sum

-- from Honsell, Lenisa, Scagnetto, [2024] "Two Views on Unification: Terms as Strategies"

record Signature : 𝒰₁ where
  field
    Symbol : 𝒰
    arity  : Symbol → ℕ

module Theory (Var : 𝒰) ⦃ d : is-discrete Var ⦄ (Sig : Signature) where
  open Signature Sig

  -- Definition 1(i): Terms TΣ
  data Term : 𝒰 where
    var : Var → Term
    con : (f : Symbol)
        → Vec Term (arity f)
        → Term

  -- Definition 1(iii-iv): Paths and Occurrences OΣ
  -- A Step is a constructor and the index of the subtree
  record Step : 𝒰 where
    constructor step
    field
      f : Symbol
      k : Fin (arity f)

  OPath : 𝒰
  OPath = List Step

  record Occurrence : 𝒰 where
    constructor _o[_]
    field
      opath : OPath
      ovar  : Var

  open Occurrence public

  -- Helper: Checking if an occurrence is in a term
  data _∈ₜ_ : Occurrence → Term → 𝒰 where
    here  : {α : Var}
          → ([] o[ α ]) ∈ₜ var α
    there : {f : Symbol} {args : Vec Term (arity f)} {p : OPath} {α : Var} {i : Fin (arity f)} 
          → ((p o[ α ]) ∈ₜ Vec.lookup args i)
          → ((step f i ∷ p) o[ α ]) ∈ₜ con f args

  -- Definition 4: From Terms to Strategies R(σ)
  -- R(σ) is the set of pairs of different occurrences of the same variable
  Strategy : 𝒰₁
  Strategy = Occurrence → Occurrence → 𝒰

  R : Term → Strategy
  R σ o₁ o₂ = (o₁ ∈ₜ σ) × (o₂ ∈ₜ σ) × (Occurrence.ovar o₁ ＝ Occurrence.ovar o₂) × (o₁ ≠ o₂)

  -- Definition 12: Occ-substitution M
  -- An occ-substitution M is induced by M_Var : Variable → Occurrence
  -- It maps u[α] to (u ++ path(M_Var α))[variable(M_Var α)]
  OccSubst : 𝒰
  OccSubst = Var → Occurrence

  -- TODO sketchy
  ap-subst : OccSubst → Occurrence → Occurrence
  ap-subst M (u o[ α ]) with M α
  ... | (w o[ β ]) = (u ++ₗ w) o[ β ]

  OccUnifier : OccSubst → Occurrence → Occurrence → 𝒰
  OccUnifier M u v = ap-subst M u ＝ ap-subst M v

{-
  lemma13-to : {M : OccSubst} {u v : Occurrence}
             → OccUnifier M u v
             → Prefix (u .opath) (v .opath) ⊎ Prefix (v .opath) (u .opath)
  lemma13-to {u = u o[ α ]} {v = v o[ β ]} e =
    {!!}
-}

  -- Definition 14(ii): Inclusion up to substitution (⊆̂)
  -- S₁ ⊆̂ S₂ if every pair in S₁ is an instance of a pair in S₂
  _⊆̂_ : Strategy → Strategy → 𝒰
  S₁ ⊆̂ S₂ =
      ∀ {u₁ v₁}
    → S₁ u₁ v₁
    → Σ[ u₂ ꞉ Occurrence ]
       Σ[ v₂ ꞉ Occurrence ]
        Σ[ M ꞉ OccSubst ]
         (S₂ u₂ v₂ × OccUnifier M u₁ u₂ × OccUnifier M v₁ v₂)

  -- Definition 14(i): Composition up to substitution (⨾̂)
  _⨾̂_ : Strategy → Strategy → Strategy
  (S₁ ⨾̂ S₂) u'' v'' =
    Σ[ u₁ ꞉ Occurrence ]
     Σ[ v₁ ꞉ Occurrence ]
      Σ[ u₂ ꞉ Occurrence ]
       Σ[ v₂ ꞉ Occurrence ]
        Σ[ M ꞉ OccSubst ]
         (S₁ u₁ v₁ × S₂ u₂ v₂ × OccUnifier M v₁ u₂ × OccUnifier M u'' u₁ × OccUnifier M v'' v₂)

  -- Definition 16: GoI-unification
  -- σ and τ GoI-unify if their variable strategies satisfy the execution formula
  GoI-unify : Term → Term → 𝒰
  GoI-unify σ τ = 
      (R σ ⊆̂ (R τ ⨾̂ (Star (R σ ⨾̂ R τ))))
    × (R τ ⊆̂ (R σ ⨾̂ (Star (R τ ⨾̂ R σ))))