Documentation

Linglib.Theories.Semantics.Dynamic.PLA.DynamicTy2

source
@[reducible, inline]
abbrev Semantics.Dynamic.PLA.MergedAssignment (E : Type u_1) :
Type u_1

PLA assignment merges variable and pronoun assignments via sum type.

  • .inl i accesses variable i
  • .inr i accesses pronoun i
Equations
Instances For
    source
    def Semantics.Dynamic.PLA.varDref {E : Type u_1} (i : VarIdx) :
    Core.DynamicTy2.Dref (MergedAssignment E) E

    Variable dref: projection at.inl i

    Equations
    Instances For
      source
      def Semantics.Dynamic.PLA.pronDref {E : Type u_1} (i : PronIdx) :
      Core.DynamicTy2.Dref (MergedAssignment E) E

      Pronoun dref: projection at.inr i

      Equations
      Instances For
        source
        def Semantics.Dynamic.PLA.termToDref {E : Type u_1} :
        Term → Core.DynamicTy2.Dref (MergedAssignment E) E

        Interpret a PLA term as a Dynamic Ty2 dref.

        Equations
        Instances For
          source
          def Semantics.Dynamic.PLA.plaPossToMerged {E : Type u_1} (p : Core.PLAPoss E) :
          MergedAssignment E

          Convert PLAPoss to merged assignment.

          Equations
          Instances For
            source
            def Semantics.Dynamic.PLA.mergedToPLAPoss {E : Type u_1} (g : MergedAssignment E) :
            Core.PLAPoss E

            Convert merged assignment to PLAPoss.

            Equations
            Instances For
              source
              theorem Semantics.Dynamic.PLA.plaPoss_roundtrip {E : Type u_1} (p : Core.PLAPoss E) :
              mergedToPLAPoss (plaPossToMerged p) = p
              source
              theorem Semantics.Dynamic.PLA.merged_roundtrip {E : Type u_1} (g : MergedAssignment E) :
              plaPossToMerged (mergedToPLAPoss g) = g
              source
              def Semantics.Dynamic.PLA.extend {E : Type u_1} (g : MergedAssignment E) (i : VarIdx) (e : E) :
              MergedAssignment E

              Functional update for merged assignments (only affects variables)

              Equations
              Instances For
                source
                def Semantics.Dynamic.PLA.evalTerm {E : Type u_1} (g : MergedAssignment E) :
                Term → E

                Evaluate a term given a merged assignment

                Equations
                Instances For
                  source
                  def Semantics.Dynamic.PLA.formulaToCondition {E : Type u_1} (M : Model E) :
                  Formula → Core.DynProp.Condition (MergedAssignment E)

                  Translate a PLA formula to a Dynamic Ty2 condition.

                  This captures when a merged assignment satisfies the formula. Note: PLA existentials check for EXISTENCE of a witness, but don't actually extend the assignment (eliminative semantics).

                  Equations
                  Instances For
                    source
                    def Semantics.Dynamic.PLA.formulaToDRS {E : Type u_1} (M : Model E) (φ : Formula) :
                    Core.DynProp.DRS (MergedAssignment E)

                    Translate a PLA formula to a Dynamic Ty2 DRS.

                    PLA updates are eliminative (they only filter, never extend assignments). This means every PLA formula translates to a TEST in Dynamic Ty2.

                    Equations
                    Instances For
                      source
                      theorem Semantics.Dynamic.PLA.formulaToDRS_atom {E : Type u_1} [Nonempty E] (M : Model E) (name : String) (ts : List Term) :
                      formulaToDRS M (Formula.atom name ts) = [fun (g : MergedAssignment E) => M.interp name (List.map (evalTerm g) ts) = true]

                      Atom translation: predicate applied to evaluated terms

                      source
                      theorem Semantics.Dynamic.PLA.formulaToDRS_neg {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) :
                      formulaToDRS M (∼φ) = [fun (g : MergedAssignment E) => ¬formulaToCondition M φ g]

                      Negation translation: test of negated condition

                      source
                      theorem Semantics.Dynamic.PLA.formulaToDRS_conj {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) :
                      formulaToDRS M (φ ⋀ ψ) = [fun (g : MergedAssignment E) => formulaToCondition M φ g ∧ formulaToCondition M ψ g]

                      Conjunction translation: test of conjoined conditions

                      source
                      theorem Semantics.Dynamic.PLA.formulaToDRS_exists {E : Type u_1} [Nonempty E] (M : Model E) (x : VarIdx) (φ : Formula) :
                      formulaToDRS M (Formula.exists_ x φ) = [fun (g : MergedAssignment E) => ∃ (e : E), formulaToCondition M φ (extend g x e)]

                      Existential translation: test for existence of witness

                      source
                      def Semantics.Dynamic.PLA.splitAssignment {E : Type u_1} (g : MergedAssignment E) :
                      Assignment E × WitnessSeq E

                      Split a merged assignment into variable and witness components

                      Equations
                      Instances For
                        source
                        theorem Semantics.Dynamic.PLA.evalTerm_eq_Term_eval {E : Type u_1} [Nonempty E] (g : MergedAssignment E) (t : Term) :
                        evalTerm g t = Term.eval (splitAssignment g).1 (splitAssignment g).2 t

                        Term evaluation agrees with PLA semantics

                        source
                        theorem Semantics.Dynamic.PLA.extend_fst_eq_update {E : Type u_1} [Nonempty E] (g : MergedAssignment E) (x : VarIdx) (e : E) :
                        (splitAssignment (extend g x e)).1 = (splitAssignment g).1[x ↦ e]

                        extend and Assignment.update align on the variable component

                        source
                        theorem Semantics.Dynamic.PLA.extend_snd_eq {E : Type u_1} [Nonempty E] (g : MergedAssignment E) (x : VarIdx) (e : E) :
                        (splitAssignment (extend g x e)).2 = (splitAssignment g).2

                        extend doesn't affect the pronoun component

                        source
                        theorem Semantics.Dynamic.PLA.formulaToCondition_eq_sat {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (g : MergedAssignment E) :
                        formulaToCondition M φ g ↔ Formula.sat M (splitAssignment g).1 (splitAssignment g).2 φ

                        Formula condition agrees with PLA satisfaction

                        source
                        theorem Semantics.Dynamic.PLA.formulaToDRS_correct {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (g h : MergedAssignment E) :
                        formulaToDRS M φ g h ↔ g = h ∧ Formula.sat M (splitAssignment g).1 (splitAssignment g).2 φ

                        PLA formula semantics corresponds to Dynamic Ty2 DRS.

                        A merged assignment g satisfies the DRS iff the split assignment satisfies the original PLA formula.