Terms over signatures

module universal-algebra.terms-over-signatures where
Imports
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)