Settheory.com

[· · · ] a transformational programming method-ology that includes a fully operational set-the-oretic proof checker [· · · ] [· · · ] examples of two moderately difficult pro- gram derivations. One of these derives a highlevel form of an algorithm to compute the bisim-ulation equivalence relation [· · · ] the other de-rives an algorithm to minimize the number ofstates in a deterministic finite state automa-ton.
[· · · ]Based on our experience with these deriva-tions, we believe that mechanical verificationof program transformations is the most impor-tant missing ingredient to the successful use oftransformational programming as part of a vi-able program development technology.
But approximately 7,000 lines of NAP textwere used [· · · ] to work out the whole proof.
We believe that this amount of “proofware”represents about ten times the size of a legi-ble mathematical proof. We would hope thata high level language approach to proof con-struction and reuse would help.
• How can we ‘tame’ the problems which arise • Is the distinction between calculus and theory • Any answer must ensue from an extensive ex- • It is convenient to move from established re- search on the foundations of mathematics andanalysis • (Hyper-)textual scenarios are more persistent • one follows the royal road of mathematics paved by the work of Cauchy, Dedekind, Frege,Cantor, Peano, Whitehead-Russell,Zermelo-Fraenkel-von Neumann, etc.
• the other aims at assessing the current state of ‘proof technology’, insisting particularly onthe equational calculus of dyadic relations • Brought into evidence the usability of set the- ory as a lingua franca for the whole of maths • Led to an extremely valuable development of • Did not impress a technological push propor- Ord(X) =: X ⊆ P(X) & (∀ y, z ∈ X) =: c ⊆ Q | (∀ y ∈ c)(∃ z ∈ c)(y < z) & (∀ y ∈ c)(∀ z ∈ Q)(z < y → z ∈ c) • Part of the appeal of set theory stems from the existence of a variant of it which deals withfinite sets only • It well bridges problem specification languages with program specification languages ( whereset-handling capabilities are the ‘bread-and-butter’ ) • Boolean operations ( save absolute comple- • extensional ∈ ( two sets cannot have the same • nesting ( which makes even individuals super- • Possibility to form sets complying with inten- arb X ∈ X with X & X ∩ arb X = ∅ s∞ = ∅ & (∀ x ∈ s∞)( {x} ∈ s∞) dem wir einen sehr zusammengesetztenSinn verbinden. Dieses Zeichen dient unssozusagen als Gef¨ We often need to associate some highly com-pound meaning with a symbol. Such a sym-bol serves us as a kind of container in whichwe can carry this meaning, always with theunderstanding that it can be opened if weneed its content.
The reader who remembers these key points will do well in what follows. In particu-lar, it is now quite all right to entirelyforget how the nonstandard universe wasdefined and to banish ultrafilters from ourconsciousness.
Martin Davis, Applied Nonstandard Analysis, 1977 THEORY orderedPair( )==> (cons, car, cdr, nl, len) car cons(X, Y ) = Xcdr cons(X, Y ) = Ycons(X, Y ) = cons(U, V ) nl = cons(X, Y )len(nl) = 0len(cons(X, Y )) = next(len(Y )) ‘Within’ orderedPair we would perhaps see Theories will form a hierarchy:‘from above’ orderedPair, we would see (or something equivalent) before the ‘invocation’ APPLY ( [ − , − ], hd , tl , [ ], ln ) Defining len(−) inside orderedPair is certainly eas-ier than outside it So far, ‘THEORY’ supplies us an extension mech-anism more flexible, but of the same nature, as • definitions such as P ∩Q =: P ∪ Q for Rob- • mechanisms such as Skolemization, which en- ∃ u ( ∀ x x · u = x & ∀ y ∃ v y · v = u ) . . . . . . However, brevity, legibility, conservativ- Definitions serve various purposes. At theirsimplest they are merely abbreviations whichconcentrate attention on interesting constructsby assigning them names which shorten theirsyntactic form. (But of course the compound-ing of such abbreviations can change the ap-pearance of a discourse completely, transform-ing what would otherwise be a exponentiallylengthening welter of bewildering formulae intoa sequence of sentences which carry helpfulintuitions). Beyond this, definitions serve to‘instantiate’, that is, to introduce the objectswhose special properties are crucial to an in-tended argument. Like the selection of cruciallines, points, and circles from the infinity ofgeometric elements that might be consideredin a Euclidean argument, definitions of thiskind often carry a proof ’s most vital ideas.
X ∈ s → Eq(X, X)X, Y, Z ∈ s & Eq(X, Y ) -- Lt is thereby assumed to be-- irreflexive and well-founded on dom A joint application of this recursive fcn and of m ⊆ n & P(m) & (∀ k ⊆ m) k = m → ¬P(k) is the (easily generalizable, and giving a Σ insen-sitive to operand rearrangement and grouping) (∀ x, y ∈ abel)(x+y ∈ abel -- closure w.r.t. . . .
u ∈ abel & (∀ x ∈ abel)(x+u = x) -- unit el’t(∀ x, y, z ∈ abel) (x+y)+z = x+(y+z) -- assoc.
& (∀ x ∈ N)(∀ y ∈ abel) Σ({[x, y]}) = y is map(F ) & Finite(F ) & range(F ) ⊆ abel Σ(F ) = Σ(F ∩ G) + Σ(F \ G) -- additivity Preliminary to a very general construction of inductive sets, we can define into-ness, injectiv-ity, inductive closedness, and surjectivity: (∀u, v ∈ S)(∀y) R(u, y) & R(v, y) → u = v A ⊆ S & Maps(R, S, S \ A) & Disj(R, S) IndEncl(N, R, A) &(∀t) A ⊆ t & Maps(R, t, t) → N ⊆ t . .
B ⊆ a → IndClosed(indCl(B), r, B)IndClosed(n, r, a) . .
X ∈ n → IndClosed(indCl({X}), r, {X}) IndClosed(n, r, a)X ∈ a → p(X)X ∈ n & p(X) & r(X, Y ) → p(Y ) a = ∅ → n = ∅Exhs(r, n \ a, n)X ∈ n → p(X) IndClosed(n, r, a)X ∈ n → IndClosed(tree(X), r, {X}) -- N.B.: this paves the way to-- recursive constructions over n IndClosed(n, r, a)X ∈ n → IndClosed(tree(X), r, {X})Y ∈ n & (∀x ∈ n) Y ∈ tree(x) \ {x} → p(x) Classical examples of inductive sets, which can be constructed and exploited by means of theabove THEORIES are: the set N of natural num-bers; the set of all finite lists with componentsdrawn from a fixed base set A; the set of all termsover a signature The obvious goal of modularization is to avoid repeating similar steps when the proofs of twotheorems are closely analogous Modularization must also conceal the details of a proof once they have been fed into the systemand successfully certified When coupled to a powerful underlying set the- ory, indefinitely expansible with new function sym-bols generated by Skolemization, the technicalnotion of “theory” illustrated above appears tomeet such proof-modularization requirements

Source: http://www.settheory.com/Omodeo/Atlanta9mar02.pdf