โ†‘ Top


Interpretation of Terms in General Structures

This is the Structures.Terms module of the Agda Universal Algebra Library.

When we interpret a term in a structure we call the resulting function a term operation. Given a term p and a structure ๐‘จ, we denote by ๐‘จ โŸฆ p โŸง the interpretation of p in ๐‘จ. This is defined inductively as follows.

  1. If p is a variable symbol x : X and if a : X โ†’ โˆฃ ๐‘จ โˆฃ is a tuple of elements of โˆฃ ๐‘จ โˆฃ, then define ๐‘จ โŸฆ p โŸง a := a x.

  2. If p = f t, where f : โˆฃ ๐‘† โˆฃ is an operation symbol, if t : (arity ๐น) f โ†’ ๐‘ป X is a tuple of terms, and if a : X โ†’ โˆฃ ๐‘จ โˆฃ is a tuple from ๐‘จ, then define ๐‘จ โŸฆ p โŸง a := (f แต’ ๐‘จ) (ฮป i โ†’ ๐‘จ โŸฆ t i โŸง a).

Thus interpretation of a term is defined by structural induction.

{-# OPTIONS --without-K --exact-split --safe #-}

module Structures.Terms where

-- Imports from Agda and the Agda Standard Library ---------------------
open import Agda.Primitive   using ( lsuc ; _โŠ”_ ; Level ) renaming ( Set to Type )
open import Structures.Basic using ( signature ; structure ; _แต’_ )
open import Terms.Basic

private variable
 ๐“žโ‚€ ๐“ฅโ‚€ ๐“žโ‚ ๐“ฅโ‚ ฯ‡ ฮฑ ฯ : Level
 ๐น : signature ๐“žโ‚€ ๐“ฅโ‚€
 ๐‘… : signature ๐“žโ‚ ๐“ฅโ‚
 X : Type ฯ‡

open signature
open structure

_โŸฆ_โŸง : (๐‘จ : structure ๐น ๐‘… {ฮฑ} {ฯ}) โ†’ Term X โ†’ (X โ†’ carrier ๐‘จ) โ†’ carrier ๐‘จ
๐‘จ โŸฆ โ„Š x โŸง = ฮป a โ†’ a x
๐‘จ โŸฆ node f t โŸง = ฮป a โ†’ (f แต’ ๐‘จ) (ฮป i โ†’ (๐‘จ โŸฆ t i โŸง ) a)


โ† Structures.Isos Structures.Substructures โ†’