3.2 ELAN Equational Specifications

An ELAN equatiomal specification is given by a many-sorted conditional Term Rewrite System.

Definition. Let Sigma be a many-sorted first-order signature, such that Sigma_S contains the sort bool and Sigma_P is empty. Let X be a set of sorted variables, where sorts are taken from Sigma_S. The set of ELAN boolean expressions EBE(Sigma,X) is the set smallest set such that:

• false e EBE(Sigma,X) and true e EBE(Sigma,X)
• If t₁:s,t₂:s e T(Sigma_F,X), then t₁=t₂ e EBE(Sigma,X)
• If f:s₁ ×...×s_n -> bool and t₁:s₁,..., t_n:s_n e T(Sigma_F,X), then f(t₁,...,t_n) e EBE(Sigma)
• If b e EBE(Sigma,X), then not  b e EBE(Sigma,X)
• If b₁,b₂ e EBE(Sigma,X), then b₁  and  b₂ e EBE(Sigma,X), b₁  or  b₂ e EBE(Sigma,X)

The set of ELAN formulas EF(Sigma,X) is the smallest set such that:

• If f: s₁ ×...×s_n -> s e Sigma_F, t₁:s₁,..., t_n:s_n,t:s are terms in T(Sigma_F,X), and b e EBE(Sigma,X), then (f(t_1,...,t_n) -> t  if  b) e EF(Sigma,X) The sort of this formula phi, denoted by sort(phi), is s.

An ELAN equational specification is given by a tuple (Sigma, V, EF) where V is a finite subset of X and EF is a finite subset of EF(Sigma,V).

Using the ELAN concrete syntax, an ELAN equational specification has to be defined as follows.

Example. (ELAN equational specification skeleton).

module Module

sort {s}(s  $e$  SigmaS) 
end

operators global 
{f}(f  $e$  SigmaF) 
end

{
rules for sort(phi)
{v}(v  $e$  V)
global
[] phi end
end
}(phi  $e$  EF) 

end // of module

On can remark that rules are grouped according to their sorts. Moreover, variables are local to a group of rules. This explains why we distribute the set of variables V involved in the terms of the TRS to each group of rules.

This program is a very restrictive form of ELAN programs, where we have

• no importation of sub-modules,
• no labelled (or named) rules and, so no strategies,
• only one rule in each group.