Constructors

Assuming that the equations in a functional module are (ground) Church-Rosser and terminating, then every ground term in the module (that is, every term without variables) will be simplified to a canonical form, perhaps modulo some declared equational attributes. Constructors are the operators appearing in such canonical forms. The operators that ``disappear'' after equational simplification are instead called defined functions. For example, typical constructors in a sort Nat are zero and s_, whereas in the sort Bool, true and false are the only constructors.

It is quite useful for different purposes, including both debugging (see Chapter 13) and theorem proving, to specify when a given operator is a constructor. This can be done with the ctor attribute. For example, we can refine our operator declarations in Section 3.4 with constructor information as follows:

  op zero : -> Zero [ctor] .
  op s_ : Nat -> NzNat [ctor] .
  op nil : -> NatSeq [ctor].
  op __ : NatSeq NatSeq -> NatSeq [ctor assoc id: nil] .

Three slightly subtle points should be mentioned, namely the relationships of constructors to operator overloading, to kinds, and to equations. The first key observation is that constructor declarations are local to given sorts for the arguments and for the result. Nothing prevents an operator from being a constructor at some level in the subsort ordering but being a defined function at another. For example, we could have declared a successor function for integers,

  op s_ : Int -> Int .

which is not a constructor. Indeed, we can define the sort Int with a subsort NzNeg of nonzero negative numbers built up with a unary minus constructor -_, and we can then specify both unary minus -_ and successor s_ as defined functions on the integers by giving the equations:

  sorts NzNeg Int .
  subsorts Nat NzNeg < Int .
  op -_ : NzNat -> NzNeg [ctor] .
  op -_ : Int -> Int .
  op s_ : Int -> Int .

  var N : Nat .

  eq - zero = zero .
  eq - (- (s N)) = s N .
  eq s (- (s N)) = - N .

A related observation is that a defined function, which totally disappears at some level in the subsort ordering, might not go away for terms at the kind level. For example, even though addition may be a defined function, we may encounter an arithmetic error expression in a kind of numbers such as

  (s s zero) + p zero

because the predecessor function p has been declared on nonzero natural numbers.

  op p : NzNat -> Nat .

The last point is that constructors may obey certain equations; that is, they do not have to be free constructors. The equations that they may obey (even as constructors, not just in other overloaded variants such as the integer successor function above) may be either equational attributes (such as the assoc attribute in the above concatenation operator for strings of natural numbers), or ordinary equations, or both. For example, we can add a sort NatSet of finite sets of natural numbers to our NUMBERS module by declaring a set union operation _;_ using equational attributes to declare that it is associative and commutative with identity the empty set, and using an ordinary equation to express idempotency.^4.6

  sort NatSet .
  subsort Nat < NatSet .
  op empty : -> NatSet [ctor] .
  op _;_ : NatSet NatSet -> NatSet [ctor assoc comm id: empty] .
  eq N ; N = N  .

Given an equational specification in which several operators have been declared as constructors by means of the ctor attribute and such that the equations are terminating, the sufficient completeness problem consists in verifying that the canonical forms of all well-typed ground terms are constructor terms. Intuitively, this means that all defined operations (i.e., those that are not declared as constructors) have been fully defined. Maude's Sufficient Completeness Checker (SCC) can be used to ensure that constructor declarations are really correct, so that all functions are fully defined relative to those constructors. We can take the NUMBERS module, incrementally introduced in Chapter 3 and the previous sections of this chapter, to illustrate how the SCC can be used to help the specifier in this regard.

  fmod NUMBERS is
    sort Zero .
    sorts Nat NzNat .
    subsort Zero NzNat < Nat .
    op zero : -> Zero [ctor] .
    op s_ : Nat -> NzNat [ctor] .
    op sd : Nat Nat -> Nat .
    ops _+_ _*_ : Nat Nat -> Nat .
    op _+_ : NzNat Nat -> NzNat .
    op p : NzNat -> Nat .

    vars I N M : Nat .
    eq N + zero = N .
    eq N + s M = s (N + M) .
    eq sd(N, N) = zero .
    eq sd(N, zero) = N .
    eq sd(zero, N) = N .
    eq sd(s N, s M) = sd(N, M) .

    sort Nat3 .
    ops 0 1 2 : -> Nat3 .
    op _+_ : Nat3 Nat3 -> Nat3 [comm] .
    vars N3 : Nat3 .
    eq N3 + 0 = N3  .
    eq 1 + 1 = 2 .
    eq 1 + 2 = 0 .
    eq 2 + 2 = 1 .

    sort NatSeq .
    subsort Nat < NatSeq .
    op nil : -> NatSeq [ctor].
    op __ : NatSeq NatSeq -> NatSeq [ctor assoc id: nil] .

    sort NatSet .
    subsort Nat < NatSet .
    op empty : -> NatSet [ctor].
    op _;_ : NatSet NatSet -> NatSet [ctor assoc comm id: empty] .
    eq N ; N = N .
  endfm

For expository reasons, since the ctor declaration had not yet been explained, some operators and constants were declared without the ctor attribute when they were introduced in Section 3.6. The SCC reports the first term it finds not reducible to a constructor. In this case, the first such report we get is the following:

  Maude> (scc NUMBERS .)
  Checking sufficient completeness of NUMBERS ...
  Warning: This module has equations that are not left-linear which
    will be ignored when checking.
  Failure: The term 0 was found to be a counterexample. Since the
    analysis is incomplete, it may not be a real counterexample.

We fix this error by adding the ctor attribute to the declaration of the constants 0, 1, and 2 of sort Nat3:

  ops 0 1 2 : -> Nat3 [ctor].

After this declaration is corrected, a more serious bug is found by the SCC, namely,

  Maude> (scc NUMBERS .)
  Checking sufficient completeness of NUMBERS ...
  Warning: This module has equations that are not left-linear which
    will be ignored when checking.
  Failure: The term zero * zero was found to be a counterexample.
    Since the analysis is incomplete, it may not be a real 
    counterexample.

This message shows that the definition of multiplication is incomplete, because we have declared the operator without the ctor attribute but we have forgotten the equations defining such operation on natural numbers. For example, we can add the following equations to make up for this omission:

  eq N * zero = zero .
  eq N * s M = (N * M) + N .

A further iteration of the SCC on the amended specification shows that the equations for the predecessor operation p are missing as well. Since p is only defined on nonzero natural numbers, only one equation needs to be added:

  eq p(s N) = N .

The corrected NUMBERS module after this analysis (together with some additional declarations introduced in the following sections) is presented in Section 4.9. Here is the tool output on the corrected module:

  Maude> (scc NUMBERS .)
  Checking sufficient completeness of NUMBERS ...
  Warning: This module has equations that are not left-linear which
    will be ignored when checking.
  Success: NUMBERS is sufficiently complete under the assumption
    that it is weakly-normalizing, confluent, and sort-decreasing.