|  | |||||||||
On the role of interpolation in stepwise refinement.
T. Dimitrakos and T.S.E. Maibaum
Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ
ftd,tsemg@doc.ic.ac.uk
Abstract
In the 25 years of its history, basic research in the Abstract Data Type community has been challenged to provide answers to some critical questions on the fundamentals of refinement between formal specifications. Such questions include: Why do correct refinements not compose correctly in all cases ? What results are dependent on the specification formalism (equational, first order, etc) and what are universal"? Which meta-logical properties of a specification formalism facilitate the refinement process? An example of a metalogical property which amounts to a law" of a general theory of specification and refinement is given by the role of interpolation in parameter instantiation and the composability of refinements. In addition, the presence of a Uniform version of Craig-Robinson interpolation is shown in [9] to facilitate the verification and construction of refinements and to underlie the potential automation of the refinement process in an appropriate entailment system.
1 A refinement paradigm
Let us consider program development by means
of stepwise refinements. One postulates some abstract
data type-like specification1 (ADT), suitable
for the problem at hand, which has to be implemented
on the available system. The end product
consists of (the text of) an abstract program
manipulating the postulated ADT, together with
a suite of (texts of) modules implementing successive
ADTs on more concrete ones until reaching the
available executable level (Target Programming
Platform", TPP). See also [18, 16, 23]. The essential
knowledge about the relevant properties of the
abstractions involved, is provided by the axioms in
the specifications. The proof that the abstract program
does exhibit the required behaviour consists
of syntactical manipulations that derive the verification
conditions from the abstract specification.
Similarly, the correctness of the implementations
of the ADTs is verified by syntactical processes, as
1Refinement of abstract data types has been the original motivation. In the context of this paper, the generic term ADT may also refer to program and systems specifications.
we shall elaborate upon in the sequel.
A closer examination of what is involved when implementing an ADT S on (in terms of) another one T, indicates that the resulting artifact is a module M that represents objects of S in terms of those of T, and operations and predicates of S by means of procedures using operations and predicative statements of T. One can abstract a little from the actual procedure texts by replacing them with specifications of their input-output behaviours. These amount to possibly incomplete definitions of the operations and predicates in S in terms of those of T and can be regarded as axioms involving both the symbols of S and T. Similarly the representation part describes the abstract" sorts in terms of the concrete" ones, which can be abstracted to axioms introducing the new sorts and capturing (some of) the so-called representation invariants [15, 17].
With this abstraction in mind, we are ready to describe this situation in terms of formal specifications, ie. logical theories presented by (finite sets of) axioms [34, 33].
One expands the language of the concrete" specification T by adding symbols to correspond to the abstract ones in S, perhaps together with some auxiliary symbols, and extends T to M by adding extension axioms which are sentences in the extended language. Since one does not want to disturb the given concrete specification T, the extension e from T to M should not impose any new constraints on T. This is formulated by requiring the extension e:T!M to be conservative [26] in the sense that M adds no consequence to T in the language of the latter.
One then needs to correlate the abstract" symbols in S to the corresponding ones in T (similarly, in some sense, to procedure headings / calls being correlated with the corresponding bodies). However, the properties of S are still important, for instance in guaranteeing the correctness of the abstract program described by S. Thus, in translating from S to M one wishes to preserve the properties of S as specified by its axioms. Hence, the translation
i from S to M should yield an interpretation of the corresponding (logical) theories, in the sense that i translates each consequence of S to a consequence of T.
The former are encapsulated in the concept of
an implementation of S on T. This consists of a
theory interpretation i from S to a conservative
extension M of T and can be presented as a tuple
a=hiff; effi of theory morphisms, one theory interpretation
iff:S!M and a conservative extension
eff:T!M, which share a common target M, called
mediating specification.
An implementation ff = hiff; effi
of S on T is depicted as an implementation
triangle" on the right,
and is often called a canonical
implementation step" [33].
S Mff
T
iffeffff
In stepwise development, it is highly desirable to
be able to compose refinement steps in a natural
way. Given an implementation ff, of S on T1 followed
by an implementation of T1 on T2, one
would like to compose these implementations in an
easy and natural way, so as to obtain a composite
implementation ffiff of S on T2. This is where
an important property, namely the Modularisation
property, comes into play:
It guarantees the composability
of refinements
by asserting that the
completion of a diagram
Mff T1 M effi
to a rectangle
heff; i0 ; i ; e0ffi, depicted
on the right, is such that
the conservativity of eff
implies the conservativity
of e0ff.
S Mff M ffiff
T1 M
T2
iffeffi0e0ffieff
Given that the Modularisation property holds, and since the class of theory interpretations, and its subclass of conservative extensions, are closed under composition, the two refinements ff, of S on T1, and , of T1 on T2, compose to a refinement ffiff of S on T2.
Shifting the focus to parameter instantiation,
the conservative extension e:P!S[P] denotes
the insertion of the formal parameter into the
parametrised specification and i:P!T is the
fitting" interpretation. The result S[T] of the
instantiation operation S[P77!T] is obtained by
completing the diagram he; ii to
the rectangle he; i0; i; e0i so that
e0:T!S[T] is a conservative extension
which captures the insertion
of T to S[T].
S[P] S[T]
P T
ei0e0i
Again, the presence of the Modularisation prop-
erty enables the correct instantiation of the formal parameter.
Another dividend stems from the fact that this view concentrates on the logical aspects of implementation. For, recall that a (conservative) extension e encodes addition of formulae rather than programs. These formulae record the design decisions taken in the implementation, not yet their actual coding into a program text. Therefore, we achieve orthogonality: the process of coding actual modules is independent of { and can proceed in parallel with { the process of further (logical) refinement. The successive refinements record the various design decisions.
2 The appearance of a universal law The first proof of what became known as the Modularisation property was put forward in 1982-83, based on an observation of Martin Sadler ([20]), and indicated a strong interconnection between the Modularisation property and interpolation: The requirement that any diagram he; ii with e conservative can be completed to a rectangle he; i0; i; e0i so that e0 is also conservative, was equivalent { in first order logic { to a very important and wellknown metalogical property of this logic that is encapsulated in what is known as the Craig Interpolation Lemma [6]. Other logics with poor interpolation properties failed to meet this requirement and this accounted for the negative results in [10].2 The initial proof indicated that, within first order logic, Modularisation was equivalent to the Craig Interpolation Lemma. Some years later the important role of the Craig Interpolation property was independently observed by a group working with Bergstra [2], who attributed the lack of certain modularity properties in their formalisms to the absence of the interpolation property. Further work on this, revealed an important observation [25]: For other logics, such as (conditional) equational, the various formulations of Craig interpolation are not equivalent. The crucial version of interpolation turned out to be the following (called splitting interpolation in [25]):
For a (first order) formula ' and sets of (first
order) formulae A; B, if A[B`FOL' then there
are (first order) formulae #1; : : : ; #n in the common
language of A[B and ' such that:
(1) A`FOL#i, 1 <= i <= n, and
(2) A[f#1; : : : ; #ng`FOL'.
Crucially, neither conditional equational logic, nor
equational logic have this property.
2The Modularisation property fails for the combination of equational logic with initial algebraic semantics on which [10] had focused.
Of even greater import for future developments, it was noted that the Modularisation result was actually asserting the preservation of conservative extensions by pushouts in the category of first order theories. The observation having being made, there was an obvious route to generalisation [13, 14, 9] (first possess in [20]) in ss?Institutions [12], and Entailment Systems [22]. This result would appear to have the status of a universal law: An Entailment System (ss-Institution) E is a triple hSign; gram; `Ei where Sign is a category of signatures, gram:Sign!Set is the grammar functor (that assigns to each signature ?, the set of well formed formulae over ?) and `E is a Sign-indexed family of binary relations such that, for every ? in Sign, `E? ? 2gram(?) ? gram(?) is reflexive, monotonic, transitive, and stable under translation. 3
An Entailment System E= hSign; gram; `Ei enjoys Craig-Robinson Interpolation iff for every pushout diagram D in Sign, depicted below, and every A ? gram(?A), B ? gram(?B), ' 2 gram(?A), such that Ai0[Be0`E?C'e0 there is a set
I(A;B;';D) ? gram(?R) of interpolants such that:
(1). A`E?AIe(A;B;';D),
and
(2). I(A;B;';D)[B`E?B'
?A ?C
D
?R ?B
ei0e0i
where, for each translation i:?1!?2 and ffi 2 gram(?1), the writing of ffi i 2 gram(?2) denotes the image of the formula ffi under the translation induced by i. Analogously, if ? ? gram(?1) then ?i = fffii : ffi 2 ?g. Finally, ?`E?? for
?; ? ? gram(?) means ?`E? ffi for each ffi 2 ?.
Notice the use of the pushout construction to capture the notion of common language" that is required for stating the property (as in [32]). Also, if E is compact4 then, for each ', the set of interpolants I(A;B;';D) is finite. Finally, if E is a weakly structural ss-Institution then the some structural axioms on D need to be accounted. (See [14])
The Modularisation property is encapsulated in this framework as the preservation of conservative extensions under pushouts:
If e:h?R; Ri!h?A;Ai is a conservative extension and D is a pushout diagram in the category of theories over an Entailment System E , then
3That is, f'g`E?'; if ? ? ? and ?`E?' then ?`E?'; if
?`E?' and ?`E? ffi, for all ffi 2 ?, then ?`E?'; and for every
i:?1!?2 in Sign, if ?`E?' then gram(i)(?)`E?gram(i)('). 4An Entailment System E is compact iff, for each signature ?, whenever ?`E?', there is a finite ? ? ? such that
?`E?'.
e0:h?B; Bi!h?C;Ai0[Be0i is also a conservative extension.
h?A; Ai h?C; Ai0[Be0i
D
h?R; Ri h?B; Bi
eii0e0
The universal law" may then be stated as follows: The Modularisation Theorem: Given an Entailment System (ss-Institution) E , E has CraigRobinson Interpolation if and only if E has Modularisation.
3 The benefits of Uniformity
Assume that E enjoys Craig-Robinson Interpolation.
Given a pushout diagram D in the category of
signatures, and A ? gram(?A), B ? gram(?B)
we say that interpolants have a uniform presentation
iff there is a set of interpolants I(A;B;D) such
that:
(1) A`E?AIe(A;B;D),
(2) I(A;B;D)`E?RI(A;B;';D) for every ' 2
gram(?B), and
(3) I(A;B;D) is finite whenever A is finite.
(ie. for each assertion ff 2 A there is a finite set
of interpolants which is independent of consequent
').
An Entailment System E enjoys Uniform CraigRobinson Interpolation iff for every A, B, D there is a uniform presentation I(A;B;D) of the interpolants.
An immediate benefit of Uniform CraigRobinson Interpolation is that conservativity can be verified [9]. For, recall that any translation e:?R!?A can be viewed as the trivial pushout of itself along the identity morphism. Hence, if (?R, e) is a subsignature of ?A then e: h?R; Ri!h?A;Ai is a conservative extension iff A interprets R under e and R entails the uniform interpolant I(A;?;e).
?A
R`E?RI(A;?;e) A`E?ARe
?R
e
Another dividend of uniformity is based on the
observation that the minimal completion of a partial
signature morphism i:?A9?B is encapsulated
into a pushout diagram, depicted below, where
(?R, e) denotes the subsignature of ?A on which i
is defined:
There exists a refinement ae=haei; aeei of h?A; Ai
on h?B; Bi that respects i
iff B`E?BIi(A;B;D).
Because conservative extensions are always
factored to conservative extensions [9, 35, 36],
the existence of a conservative aee forces e0 to
be conservative, and the requirement that e0 is
conservative is equivalent to B interpreting the
uniform interpolant I(A;B;D) under i. (See [9] for
details of the proof.)
M
h?A; Ai h?C; Ai0[Be0i
D
h?R; I(A;B;D)i h?B; Bi
eie0i09!aeiaee
The potential benefits of a Uniform version of Craig-Robinson interpolation for the refinement of specifications [8, 9] are hindered by its absence from many expressive logics: For example, classical and Heyting's intuitionistic propositional logic have a Uniform version of Craig-Robinson interpolation, whereas (conditional) equational, and classical/intuitionistic first order logics do not. This motivates a thorough investigation [9] of adequate expansions of known entailments, so that an easyto-derive uniform presentation of the interpolants is supported.
3.1 Uniformity and Subentailments
An obvious question to ask if one's favorite formalism does not possess this crucial modularity property is how to fix" it. There are two obvious possibilities: either extend the formalism to one which does have the property, or alternatively, restrict the specifications which are acceptable" to a subclass which enjoy this property. The emergence of the work on persistence [11] reflects the latter design" choice. But let us consider the first design" choice (expansion) and view the appropriate restriction of acceptable" specifications retrospectively. First, we need to place uniform interpolation in the perspective of Subentailment Systems5 [22] which formalise expansion of logical formalisms.
A simple case of a Subentailment System is
obtained when extending an Entailment System
EO conservatively to an Entailment System E ,
without changing the corresponding alphabets:
? Both EOand E share the same category of
signatures, Sign;
?The gramO grammar functor of E extends
the gramO of EO so that gramO(i) =
5A Subentailment System [22] hEO;Ii of an Entailment
System E consists of an Entailment System EOand a subentailment
morphism I: EO!E. The latter involves an embedding
functor J:SignO!Sign, which induces a natural
transformation of formulae ?J:gramO!gram and is such
that `EJ(?) is conservative over `EO
? for each ? of SignO .
gram(i) (gramO(?1) ? gramO(?2)) for every i:?1!?2 in Sign;
Sign * ? Setgram
gramO
? The entailment `E is conservative over the `EO
entailment
(ie, `EO
? = `EM
? ?2gramO(?1) ? gramO(?2)? for
every signature ? in Sign).
The above expansion of EO to E induces an adjoint situation (?) ?[ (?)o 6 where, for every EO- theory h?; Aoi, the writing of h?; Aoi denotes the closure of Ao under `E? , and, for every E-theory h?; Ai, the writing of h?; AiO denotes its EO- reduct7. By the conservativity of `E over `EO ,
both h?; Aoi and
?
h?; Aoi
?
O present the same
EO-theory.
Now, assume that EO lacks Craig-Robinson Interpolation and E provides uniform interpolants in derivations between EO-sentences.
Since EO lacks Craig-Robinson Interpolation one
would not expect all refinements between EO-
theories to compose. On the other hand, all E-
refinements compose. And the restriction of an
E-refinement ff over EO yields the EO-refinement
ff. Hence, to ensure that two subsequent EO-
refinements, ff of S on T1 and of T1 on T2, compose,
reduces to detecting that ff and are EO-
reducts of two subsequent E-refinements, ff of S on
T1 and of T1 on T2. The latter is obtained [9] by
the following proof obligation:
Two subsequent EO-refinements ff and compose
correctly iff M `E?M Ii (Mff;M ;D)
Mff ?Mff ?M
D
I(Mff;M ;D) ?T1 ?M M
effii0e0ff
Notice that both M and Mff are EO- axiomatisations, the uniform presentation of the interpolants consists of E -, rather than EO-, sentences and so the proof obligation is on the E-entailment `E instead of EO.
The crucial property of the (?) functor underlying the above proof obligation, is that (?) reflects but
6If theories are viewed as structured ( sets of sentences
) by the entailment, then the tuple ?(?); (?)o? is a Galois
correspondence.
7ie. h?;AiO = h?;f'o 2 gramO(?) : A`E?'ogi.
does not preserve conservative extensions. The EO- conservative extensions preserved are exactly those which are stable under pushouts. Hence, the conservative extensions detected by (?) are those subclass of EO-refinements involved in the closed under composition.
Generalising, one can distinguish the Ro class of EO-refinement that always compose correctly. These obey the following universal property[9]: An EO-refinement ff of S on T belongs in Ro iff ff is an E-refinement of S on T.
To classify an S!M T diagram on EO as an Rorefinement is then reduced to verifying S!M T as an E-refinement which is now feasible, as illustrated at the beginning of Section 3, since E enjoys Uniform interpolation8.
4 Conclusion & Further work In this paper we presented, retrospectively, the emergence of a strong connection between some basic modularity properties and interpolation. The connection between Modularisation and CraigRobinson interpolation was revisited and restated in a general logic-independent" framework; its strength has been reestablished in the form of a universal law". Furthermore, the presence of uniform interpolants gives rise to certain proof obligations which suffice to establish the correctness of (composite) refinements [9, 8]. Having the proof obligations derived, one is justifiably concerned about the underlying computations.
An important computational issue { which arises even if EO itself enjoys uniform interpolation { is the difficulty of deriving (uniform) interpolants. The derivation of interpolants is known to be computationally hard. One would then expect the derivation of uniform interpolants to be even more complex. In an attempt to compensate for this inadequacy, we focused on generic methods to expand EO so that an easy-to-derive form of uniform interpolants is available in the expansion E .
A potential breakthrough emerges from the concept of a Development Workspace described in [9]. The latter is a Subentailment System hEO; J i such that J :EO!E expands the EO-syntax with additional logical operators, leaves the extra-logical symbols intact, and extends `EO conservatively. The form of the expansion is such that, not only does E enjoy uniform interpolation, but also all the crucial uniform interpolants in E are instances of a
8The same universal property holds even if E enjoys a non-uniform version of Craig-Robinson interpolation. But then the detection of EO-refinements closed under composition cannot be reduced to some reasonable proof obligation(s), due to the absence of uniform interpolants.
common syntactic from. The usually complex process of deriving (uniform) interpolants is thus trivialised. The latter is compatible with the insight of [24] and the remark of [7] that uniform interpolants seem to have the same implicit (meta)form. There is just one proviso, namely that in [9] this common form can be stated explicitly in the formal syntax of E . The idea of a Development Workspace seems to suit a large class of Entailment Systems and we have some evidence of its effectiveness.
Further evidence on the applicability of this construction stems from [1], where Basin and Matthews add some meta-theoretic facilities to first order logic, by extending the intuitionistic LJ to a weak second order LJ2, reflecting how some theorem provers handle meta-variables. Although this extension had been independently developed and with different motives, it was easy to show [9, 8] that, for the corresponding Entailment Systems, the expansion described in [1], was exactly the instance of a Development Workspace built over first order logic. They had shown in [1] that LJ2 is conservative over LJ and, furthermore, the positively occurring second order variables (predicatevariables") are realisable over LJ. So, if B is a set of first order axioms and 92{A is a ?11 consequent of B in LJ2, and { occur positively in A, then a first order witness-formula can be extracted from the proof B`LJ292{A (extending [21]). LJ2 is also shown to be conservative over the classical first order LK in which case all arbitrary occurrences of { are realisable. As shown in [9] (also metnioned in [8]), a uniform interpolant I(A;?;?Rae?A), for any first order A, is the obvious ?11 sentence. 92{1 : : : 92{n (A[p177!{1; : : : ; pn77!{n]), where fp1; : : : ; png is the difference in the two alphabets (of ?R and ?A), and (pi77!{i) denotes the grammatical replacement of all occurrences of a predicate symbol pi by the same (new) predicate variable {1. See [9, 8].
Potential practical applications in Computer Science include the joint extension of systems development environments [31] and algorithmic design tools [27, 30, 29, 28] so that more general and complex refinements are supported. For example, SpecWare[31] works in a similar spirit but supports only refinements ff=hiff; effi such that eff is an extension by (external) definitions, and KIDS [27, 28] is based on (first order) Unskolemization [3, 5, 19, 4, 28] which can be easily extended, within a Development Workspace, so that non-skolem EO- functions and EO-predicates are also abstracted and, depending on the status of EO, give rise to the extractions of definition-bodies as witnesses of an EO-realisation.
References
[1] David Basin and Se?an Matthews. Adding metatheoretic facilities to first-order theories. Journal of Logic and Computation, 6(6), 1996.
[2] J.A. Bergstra, J. Heering, and P. Klint. Module algebra. ACM, 37(2):335{372, 1990.
[3] W. Bledsoe and M. Ballantyne. Unskolemizing. Technical report, University of Texas at Austin, 1978.
[4] Ritu Chadha. Applications of Unskolemization. PhD thesis, University of North Carolina at Chapel Hill, 1991.
[5] P.T. Cox and T. Pietrzykowski. A complete nonredundant algorithm for reversed skolemization. Theoretical Computer Science, 28, 1984.
[6] W. Craig. Three uses of the Herbrand-Getzen theorem in relating model theory and proof theory. Journal of Symbolic Logic XXII, pages 269{285, 1957.
[7] Giovanna D'Agostino and Marco Hollenberg. Uniform interpolation, automataand the modal ?-calculus, May 1996. http://www.phil.ruu.nl/home/marco/.
[8] T. Dimitrakos. Craig-Robinson interpolation vs. Modularisation and the construction of refinemetns. Schloss Dagstuhl seminar on Logic for System Engineering", March 1997. Dagstuhl Seminar report 9710.
[9] T. Dimitrakos. Formal support for specification design and implementation. PhD thesis, Imperial College, 1997. In preparation.
[10] H.-D. Ehrich. On the theory of specification, implementation and parametrization of abstract data types. J.ACM, 29(1), 1982.
[11] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specifications. EATCS, Monographs on Theoretical Computer Science. Springer-Verlag, 1985.
[12] J.L. Fiadeiro and A.Sernadas. Structuring theories on consequence. In D. Sannella and A. Tarlecki, editors, Recent Trends in Data Type Specification, pages 44{72, 1988.
[13] J.L. Fiadeiro and T.S.E. Maibaum. Stepwise program development in ss-institutions. Technical report, Imperial College, 1990.
[14] J.L. Fiadeiro and T.S.E. Maibaum. Generalising interpretations between Theories in the Context of (ss)institutions. In S. Gay G. Burn and M. Ryan, editors, Theory and Formal Methods, pages 126{147. SpringerVerlag, 1993.
[15] J.V. Guttag. Abstract data types and the development of data structures. Comm. Assoc. Comput. Mach., 20(6), 1977.
[16] J.V. Guttag and J.J. Horning. The algebraic specification of abstract data types. Acta Informatica, 10(1):27{52, 1978.
[17] J.W. Thatcher J.A. Goguen and E.G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In Current Trends in Programming Methodology, volume IV: Data Structuring. Prentice Hall, 1978.
[18] B. Liskov and S. Zilles. Programming with abstract data types. ACM, 9(4):50{59, 1974.
[19] W. W. MacCune. Un-skolemizing clause sets. Information Processing Letters, 29, 1988.
[20] T.S.E. Maibaum and M.R. Sadler. Axiomatising specification theory. In H.J. Kreowski, editor, Recent Trends in Data Type Specification, pages 171{177. SpringerVerlag, Berlin, 1985.
[21] Z. Manna and R. Waldinger. Special relations in automated deduction. Journal of the ACM, pages 1{59, January 1986.
[22] Jose Meseguer. General logics. In H.D. Ebbinghaus, editor, Logic Colloquium'87, pages 275{329, 1989.
[23] T.H.C. Pequeno and C.J.P. Lucena. An approach for data type specification adn its use in program verification. Information Processing Letters, 8(2):98{103, 1979.
[24] A. Pitts. On an interpretion of second order quantification in first order intuitionistic propositional logic. Journal of Symbolic Logic, 57:33{52, 1992.
[25] P.H. Rodenburg and R.J. van Galbbeek. An Interpolation Theorem in Equational Logic. Technical Report CS-R8838, Centre for Mathematics and Computer Science, P.O. Box 4079, 1009 AB Amsterdam, The Netherlands, 1988.
[26] J.R. Shoenfield. Mathematical Logic. Addison-Wesley, Publishing Company, 1967.
[27] D. R. Smith. KIDS: A semiautomatic program development system. IEEE Transactions on Software Engineering, 16(9):1024{1043, September 1990.
[28] D. R. Smith. Classification approach to design. Technical report, Kestrel Institute, November 1993.
[29] D. R. Smith. Constructing specification morphisms. Symbolic Computation, 15(5-6):571{606, May-June 1993.
[30] D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer programming, 14(2-3):305{321, September 1990.
[31] Yellamraju V. Srinivas and Richard Jullig. SpecWareTM: Formal suport for composing software. In Mathematics of Program Construction, July 1995. (KES.U.94.5).
[32] A. Tarlecki. Bits and pieces of the theory of institutions. In Workshop on Category Theory and Computer Science, LNCS 240. Springer-Verlag, 1986.
[33] W ladys law M. Turski and Thomas S. E. Maibaum. The Specification of Computer Programs. Addison-Wesley, 1987.
[34] P.A.S. Veloso, T.S.E. Maibaum, and M.R. Sadler. Program development as theory manipulations. In 3rd International Workshop on Software Specification and Design, 1985.
[35] P.A.S. Veloso and S.R.M. Veloso. On conservative and expansive extensions. O que no faz pensar: Cadernos de Filosofia, 4:87{106, 1991.
[36] P.A.S. Veloso and S.R.M. Veloso. Some remarks on conservative extensions: a Socratic dialogue. Bull. ETACS, 43:189{198, 1991.