Terms over signatures

module universal-algebra.terms-over-signatures where

open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.unit-type
open import foundation.universe-levels

open import linear-algebra.functoriality-vectors
open import linear-algebra.vectors

open import lists.lists
open import lists.lists-discrete-types

open import universal-algebra.models-of-signatures
open import universal-algebra.signatures

Idea

A term in a signature, is an abstract representation of a well formed expression which uses only variables and operations in the signature. For this particular formalization, we are using de Bruijn variables.

Definitions

Terms

module _
  {l1 : Level} (Sg : signature l1)
  where

  data Term : UU l1 where
    var-Term : ℕ → Term
    op-Term : is-model Sg Term

  de-bruijn-variables-term : Term → list ℕ

  de-bruijn-variables-term-vec : {n : ℕ} → vec Term n → list ℕ

  de-bruijn-variables-term (var-Term x) = cons x nil
  de-bruijn-variables-term (op-Term f x) = de-bruijn-variables-term-vec x

  de-bruijn-variables-term-vec empty-vec = nil
  de-bruijn-variables-term-vec (x ∷ v) =
    union-list
      has-decidable-equality-ℕ
        (de-bruijn-variables-term x)
        (de-bruijn-variables-term-vec v)

  arity-term : Term → ℕ
  arity-term t = length-list (de-bruijn-variables-term t)

Assignment of variables

An assignment of variables, assigns each de Bruijn variable to an element in a type.

  assignment : {l2 : Level} → (A : UU l2) → UU l2
  assignment A = ℕ → A

Evaluation of terms

Given a model of a type A and an assignment of variables, any term can be evaluated to a concrete element of the type A.

  eval-term :
    {l2 : Level} → {A : UU l2} →
    is-model Sg A → assignment A → Term → A

  eval-vec :
    { l2 : Level} → {A : UU l2} {n : ℕ} →
    is-model Sg A → assignment A → vec Term n → vec A n

  eval-term m assign (var-Term n) = assign n
  eval-term m assign (op-Term f x) = m f (eval-vec m assign x)

  eval-vec m assign empty-vec = empty-vec
  eval-vec m assign (x ∷ v) =
    eval-term m assign x ∷ (eval-vec m assign v)

  eval-vec-map-vec-eval-term :
    { l2 : Level} {A : UU l2} {n : ℕ} →
    (m : is-model Sg A) → (assign : assignment A) → (v : vec Term n) →
    eval-vec m assign v ＝ map-vec (eval-term m assign) v
  eval-vec-map-vec-eval-term m assign empty-vec = refl
  eval-vec-map-vec-eval-term m assign (x ∷ v) =
    ap (eval-term m assign x ∷_) (eval-vec-map-vec-eval-term m assign v)

Evaluation for constant terms

If a term t uses no variables, then any model on a type A assigns t to an element of A.

  eval-constant-term :
    { l2 : Level} {A : UU l2} →
    ( is-model Sg A) →
    ( t : Term) →
    (de-bruijn-variables-term t ＝ nil) →
    A

  eval-constant-term-vec :
    { l2 : Level} {A : UU l2} {n : ℕ} →
    ( is-model Sg A) →
    ( v : vec Term n) →
    ( all-vec (λ t → is-nil-list (de-bruijn-variables-term t)) v) →
    vec A n

  eval-constant-term m (op-Term f x) p =
    m f (eval-constant-term-vec m x (all-vec-lemma x p))
    where
    all-vec-lemma :
      { n : ℕ}
      ( v : vec Term n) →
      ( de-bruijn-variables-term-vec v ＝ nil) →
      all-vec (λ t → is-nil-list (de-bruijn-variables-term t)) v
    all-vec-lemma empty-vec p = raise-star
    all-vec-lemma (x ∷ v) p =
      pair
        ( pr1 (is-nil-lemma p))
        ( all-vec-lemma v (pr2 (is-nil-lemma p)))
      where
        is-nil-lemma =
          is-nil-union-is-nil-list
            ( has-decidable-equality-ℕ)
            ( de-bruijn-variables-term x)
            ( de-bruijn-variables-term-vec v)

  eval-constant-term-vec m empty-vec p = empty-vec
  eval-constant-term-vec m (x ∷ v) (p , p') =
    eval-constant-term m x p ∷ eval-constant-term-vec m v p'

The induced function by a term on a model

  vec-assignment :
    {l2 : Level} {A : UU l2} →
    ℕ → (l : list ℕ) →
    vec A (succ-ℕ (length-list l)) → assignment A
  vec-assignment x nil (y ∷ empty-vec) n = y
  vec-assignment x (cons x' l) (y ∷ y' ∷ v) n
    with
    ( has-decidable-equality-ℕ x n)
  ... | inl p = y
  ... | inr p = vec-assignment x' l (y' ∷ v) n

  induced-function-term :
    {l2 : Level} → {A : UU l2} →
    is-model Sg A → (t : Term) →
    vec A (arity-term t) → A
  induced-function-term {l2} {A} m t v with
    ( has-decidable-equality-list
      has-decidable-equality-ℕ
      (de-bruijn-variables-term t) nil)
  ... | inl p = eval-constant-term m t p
  ... | inr p =
    eval-term m
      ( tr
        ( λ n → vec A n → assignment A)
        ( lenght-tail-is-nonnil-list (de-bruijn-variables-term t) p)
        ( vec-assignment
          ( head-is-nonnil-list (de-bruijn-variables-term t) p)
          ( tail-is-nonnil-list (de-bruijn-variables-term t) p))
          ( v))
      ( t)

  assignment-vec :
    {l2 : Level} {A : UU l2} →
    (l : list ℕ) →
    assignment A →
    vec A (length-list l)
  assignment-vec nil f = empty-vec
  assignment-vec (cons x l) f = f x ∷ assignment-vec l f

Translation of terms

translation-term :
  { l1 l2 : Level} →
  ( Sg1 : signature l1) →
  ( Sg2 : signature l2) →
  is-extension-signature Sg1 Sg2 →
  Term Sg2 → Term Sg1

translation-vec :
  { l1 l2 : Level} →
  ( Sg1 : signature l1) →
  ( Sg2 : signature l2) →
  { n : ℕ} →
  is-extension-signature Sg1 Sg2 →
  vec (Term Sg2) n → vec (Term Sg1) n

translation-term Sg1 Sg2 ext (var-Term x) = var-Term x
translation-term Sg1 Sg2 ext (op-Term f v) =
  op-Term (emb-extension-signature Sg1 Sg2 ext f)
    ( tr (vec (Term Sg1))
      ( arity-preserved-extension-signature Sg1 Sg2 ext f)
      ( translation-vec Sg1 Sg2 ext v))

translation-vec Sg1 Sg2 ext empty-vec = empty-vec
translation-vec Sg1 Sg2 ext (x ∷ v) =
  ( translation-term Sg1 Sg2 ext x) ∷
    ( translation-vec Sg1 Sg2 ext v)