Documentation

ISAR.TRSView

source
inductive ISAR.TTerm :
Type

A simple term rewriting language representing the pure SKI combinator terms.

Instances For
    source
    def ISAR.instDecidableEqTTerm.decEq (x✝ x✝¹ : TTerm) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance ISAR.instDecidableEqTTerm :
      DecidableEq TTerm
      Equations
      source
      @[implicit_reducible]
      instance ISAR.instReprTTerm :
      Repr TTerm
      Equations
      source
      def ISAR.instReprTTerm.repr :
      TTerm → ℕ → Std.Format
      Equations
      Instances For
        source
        def ISAR.trs_encode :
        TTerm → ISKSubtype

        Compile/encode a TTerm into the substrate fragment ISKSubtype.

        Equations
        Instances For
          source
          def ISAR.decode_raw_val :
          ITerm → TTerm

          Constructive decoder over the ITerm structure.

          Equations
          Instances For
            source
            def ISAR.decode_raw (t : ISKSubtype) :
            TTerm

            Decode an ISKSubtype back to TTerm.

            Equations
            Instances For
              source
              theorem ISAR.decode_raw_trs_encode (t : TTerm) :
              decode_raw (trs_encode t) = t

              Proof that decode_raw after trs_encode is the identity on TTerm.

              source
              theorem ISAR.trs_encode_decode_raw_val (t : ITerm) (h : ISKTerm t) :
              ↑(trs_encode (decode_raw_val t)) = t

              Proof that trs_encode after decode_raw is the identity on ISKSubtype.

              source
              theorem ISAR.trs_encode_decode_raw (t : ISKSubtype) :
              trs_encode (decode_raw t) = t
              source
              def ISAR.trs_obs_eq (t1 t2 : TTerm) :
              Prop

              The observational equivalence relation on TTerm, reducing to operational equivalence of encodings.

              Equations
              Instances For
                source
                theorem ISAR.trs_obs_equiv :
                Equivalence trs_obs_eq

                Proof that trs_obs_eq is an equivalence relation.

                source
                def ISAR.trsObsSetoid :
                Setoid TTerm

                Setoid of TRS observations (OperEq of encodings).

                Equations
                Instances For
                  source
                  @[reducible, inline]
                  abbrev ISAR.TTermObs :
                  Type

                  Observation space: TTerm modulo observational equivalence.

                  Equations
                  Instances For
                    source
                    def ISAR.trs_decode (q : InvariantLayer) :
                    TTermObs

                    Decode an OperEq-class to a TRS observation. Well-defined because trs_encode ∘ decode_raw = id on ISKSubtype, so OperEq of substrate terms induces trs_obs_eq of decodings — no canonical_rep / choice.

                    Equations
                    Instances For
                      source
                      def ISAR.TRS_Dialect :
                      Dialect

                      The concrete TRS_Dialect : Dialect instance (computable; OperEq observations).

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For