A relation is computable iff for a given the set can be enumerated by some terminating procedure. To discuss computability it is useful to look a bit more careful at the relations we are interested in. These relations are all binary relations between feature structures. However, in the case of the relation between strings and logical forms, strings will always be related to logical forms and logical forms will be related to strings. Similarly for the relation between Dutch and Spanish logical forms. Clearly, the domain and range of the relation is structured and can be partioned into two sets and , for example the set of feature structures representing strings and the set of feature structures representing logical forms. The relation can be partitioned similarly into the relations and its inverse, . The problem to compute is now replaced by two problems: the computation of and . For example the problem to compute the relation between logical forms and strings consists of the parsing- and generation problem. It is now possible to incorporate the notion of equivalence, to obtain a definition of a parser, generator and translator. For example, an algorithm that computes the foregoing relation will enumerate for a given features structure all feature structures , such that and and are equivalent. In the case of strong equivalence this implies that (completeness), and (coherence). In other words, the input should not be extended (coherence) and should completely be derived (completeness). This usage of the terms completeness and coherence was introduced in . In the following I will discuss ways to obtain computability of one such partition.
It is well known that relations defined by unrestricted unification grammars are not computable in general as such grammars have Turing power ; it is thus not decidable whether the relation is defined for some given input. Usually some constraint on grammars is defined to remedy this. For example the off-line-parsability constraint  ensures that the recognition problem is solvable. Moreover this constraint also implies that the parsing problem as defined here is computable; i.e. the proof procedure will always terminate (because the constraint implies that there is a limit to the depth of possible parse trees for all strings of a given length).
However the off-line-parsability constraint assumes a context-free base of the formalism. A generalization of the off-line-parsability constraint for any binary relation defined by unification grammars will consist of three parts; the first and third of these parts are usually implicit in the case of parsing.
First, the value of the input must be built in a well-behaved compositional way. For example in the case of parsing: each daughter of a rule dominates part of the string dominated by the mother of that rule. Similarly for transfer and generation: each daughter of a rule has a value for that is part of the value of of the mother.
Second, a special condition is defined for rules where the input value of the mother is the same as the input value of one of the daughters. For parsing such rules have exactly one daughter. A chain of applications of such rules is disallowed by some constraint or other; this is the core of most definitions of the off-line parsability constraint. For example in  such a chain is disallowed as the principal functor of a term may only occur once in a chain. For a slightly more general definition, cf. . For generation and transfer a similar constraint can be defined. In the terminology of  the `head' of a rule is a daughter with the same logical form as its mother. A chain of these heads must be disallowed.
Third, the input should not get extended during the proof procedure. In the case of parsing this is achieved easily because the input is ground . For generation and transfer this is not necessarily the case. This is the point where the usefulness of the coherence condition comes in; the coherence requirement explicitly states that extension of the input is not allowed. For this reason strong reversiblity may be easier to obtain than weak reversibility. In the next subsection I will discuss two relaxations of strong symmetry that will not affect the computability properties discussed here.
Generalizing the terminology introduced by  a proof procedure is strongly stable iff it always terminates for grammars that adhere to a generalized off-line parsability constraint. In  a general proof procedure for DCG based on head-driven generation  is defined that is strongly stable for a specific instantiation of the generalized off-line parsability constraint.