5.9 Effectiveness

Defining an abstract syntax as a type system is not sufficient for practical applications. As the goal of an abstract syntax is to allow to represent programs or structural documents, one will want to be able to construct ground terms belonging to the syntax that is defined. This property is called effectiveness  and is required to get the induction principle often used when reasoning and proving properties of programming languages or of programs.

Note that a non-effective syntax can become effective when it is extended. The following syntax is not effective as it does not contains ground terms:

abstract syntax of L is

f : X -> X;

end L;

We can extend this syntax, adding an atomic operator:

abstract syntax of L'
  extends L with

z : -> X;

end L;

The resulting abstract syntax is now effective as it contains ground terms.