Signatures, Algebra, Homomorphisms
Signatures, Algebra, Homomorphisms
Signatures, Algebra, Homomorphisms
(*
We first fix the symbols which any candidate (abstract) language will use:
Definition: Signature ∑ - a set of symbols,
and for each symbol, its arity ≥ 0
*)
(*
We now discuss the meaning of expressions in any language whose symbols have
been specified using a signature ∑.
Semantics
Definition (∑-algebra)
A — a carrier set, and
for each 0-ary symbol in ∑, associate some element of A
for each k-ary symbol in ∑, associate a total function in A k → A
Notes:
• Not all elements of A require having a 0-ary symbol in ∑ associated with them.
That is, the carrier set may contain values (perhaps infinitely many) for which
there is no syntax. Irrational real numbers are a good examples — there may be
no way of writing a symbol for each irrational number. In fact, we may not even
be able to write an expression for each irrational number.
• Different 0-ary symbols in ∑ do not necessarily have to be associated with
different elements — two different symbols can be mapped to the same value.
Similarly for k-ary symbols, two different symbols can be mapped to the same
function.
• Two ∑-algebras can have the same carrier set A, but differ on the interpretation of
the symbols in the signature ∑. These would be considered different ∑-algebras.
*)
(*
Note: Symbols do not inherently carry meaning. We can assign whatever meanings
we choose to …. but once we assign meaning by choosing a particular ∑-algebra, we
have fixed the meanings of the symbols.
(*
Notation:
If = ⟨A, …⟩ is a ∑-algebra, and a ∈ A is associated with 0-ary symbol c in ∑, we
write c to denote the element a ∈ A, highlighting that this is the meaning
associated with symbol c in algebra .
Similarly, if f is a k-ary symbol in ∑, and in ∑-algebra = ⟨A, …⟩, f is associated
k
with a total function g : A → A, we write f to denote this function g.
*)
(* Abstract Syntax, abstractly and formally
(* Note that we have a new family of base cases: variables, which are denoted using
the parameterised constructor V(_) which takes arguments of type string.
*)
(* The corresponding Concrete Syntax can also be extended
E —> T
E —> T + E
T —> F
T —> F * T
F —> n
F —> v // a family of variables
F —> ( E )
*)
(*
We now extend the syntactic functions on tree-structured expressions *)
(* size, as before, returns the number of nodes in the tree, with a variable counted
as a single node. *)
let rec size t = match t with
N _ -> 1
| V _ -> 1
| Plus(t1, t2) -> (size t1) + (size t2) + 1
| Times(t1, t2) -> (size t1) + (size t2) + 1
;;
(* ht, also as before, returns one less than the number of levels in the tree, with
variables being treated as leaf nodes. *)
(* As mentioned before, both size and ht are good measures for performing
induction on trees. *)
(* We now define a syntactic function on exp called vars which returns the list of
variables in the tree. (We will later see that we really want a function returning the
set of variables in a syntax tree. If we represent sets as lists, then the difference
goes away; of course, we must avoid duplicates and not care about the relative order
in which elements appear). *)
let rec vars t = match t with
N _ -> [ ]
| V x -> [x]
| Plus(t1, t2) -> (vars t1) @ (vars t2)
| Times(t1, t2) -> (vars t1) @ (vars t2)
;;
(* Let us now abstract this treatment to arbitrary abstract syntax trees over
arbitrary signatures ∑. We do so by defining a set TreeΣ( ).
Uniqueness of ρ ̂
Induction Hypothesis:
Assume that for all t’ in TreeΣ( ) such that (ht t) ≤ n,
ρ (̂ t’ ) = j( t’ )
(* Only those variables that appear in a tree (term, expression) matter in its
evaluation.
Lemma (Relevant Variables): Suppose ∑ is an arbitrary signature and is the
set of variables.
Let t in TreeΣ( ) be an arbitrary tree (term, expression).
Let V = vars( t ).
Consider any ∑-algebra ℬ = ⟨B, …⟩, and let ρ1, ρ2 ∈ → B be any two B-
valuations such that for all variables x ∈ V, ρ1(x) = ρ2(x).
[Note: ρ1(y) and ρ2(y) may be very different for y ∉ V. ]
Then ρ1 ̂(t) = ρ2 ̂(t).