TECHNISCHE HOGESCHOOL EINDHOVEN Onderafdeling der Wiskunde
Memorandum 1977-14 oktober 1977
Een aanzet tot bewijsanalyse door R.P. Nederpelt
Technische Hogeschool Onderafdeling der Wiskunde PO Box 513, Eindhoven Nederland
Een aanzet tot
bewijsanaly~
R.P. Nederpelt I. Inleiding
In systemen van natuurlijke deductie, oorspronkelijk ontworpen door Jaskowski en door Gentzen, vindt men een formalisering van de
~~ebruikelijke,
intui tieve manier van redeneren in de wiskunde. De ui twendige bouw van een bewij s hangt in zo een systeem vooi--eenbelangrijk- deel af van de structuur van het te bewijzene. Om bijvoorbeeld V A [P(x)J te bewijzen, zal de aanname XE
"Laat x
E
A" meestal een geschikt uitgangspunt zijn; am a v b te bewijzen
kan men la onderstellen, om vervolgens te proberen b af te leiden. Het bestaan van dit soort wetten brengt met zich mee dat de heuristiek van een bewijs sterk beinvloed wordt door (de vorm van) het te bewijzene. Het is, zo gezegd, een goed idee am te proberen "naar het antwoord tot te werken". In eenvoudige propositie- of predikatenlogica werkt een strategie die berust op bovenstaande overwegingen vaak verblufferid snel, In dit memorandum vragen we ons af of er oak een wiskundig-technische lijn valt te ontdekken in bewijzen van meer gecompliceerd karakter. Om .dat na te gaan hebben we enige bewijzen ontleed die voorkomen in Juttings "vertaling" van Landau's boek "Grundlagen der Analysis", [IJ. De vertaling door L.S. Jutting [2J vond plaats in de wiskundige taal AUT-QE, een formeel notatie-systeem, verwant aan natuurlijke deductie-systemen en bedoeld om wiskundige teksten geformaliseerd weer te geven (zie N.G. de Bruijn [3J). AUT-QE is volledig in die zin, dat elk stuk AUT-QE-tekst verantwoord kan worden op grond van de grammaticale regels. Een gevolg is dat teksten in AUT-QE op grammaticale juistheid geverifieerd kunnen worden door een (reken-)machine. Dit brengt met zich mee dat ook een wiskundige tekst gecontroleerd kan worden, door de tekst am te schrijven in AUT-QE en daarna te verifieren. Hierin ligt een belangrijk aspect van AUT-QE. 2. De taal AUT-SL AUT-QE is een praktische taal, gemaakt om het proces van vertalen van een wiskundige tekst eenvoudig te houden en am de vertaling niet teveel van het origineel te laten afwijken. Maar als het doel is om de eigenschappen en de reikwijdte van AUT-QE-achtige talen te onderzoeken, is het minder van belang hoe dicht zo een taal bij de gebruikelijke wiskundige manier van schrijven (en denken) staat. Dan gaat het meer om helderheid van structuur, eenvoud en overzichtelijkheid van de taal zelf.
- 2 -
Voor het bovengestelde doel, de analyse van bewijzen, hebben we daarom gekozen voor een variant van AUT-QE, ontwikkeld door Nederpelt [4J en de Bruijn [5J. Een vergelijkbare taal is beschreven en onderzocht in Nederpelt [6J. We zullen deze taal hier, in navolging van de Bruijn, met AUT-SL aanduiden. De taal AUT-SL mist de duplicaties "blokopeners vs. ab:;tracties lt en "substituties vs. applicaties". Het systeem van afkorten door weglating van contextvariabelen wordt niet gebruikt in AUT-SL. We merken op dat de vorm van AUT-SL die we hier kiezen, een directe pendant is van AUT-QE en daarom we! beschikt over de mogelijkheid van type-inclusie. (De talen uit [5J en [6J kennen geen type-inclusie.) Definities zijn in AUT-SL optionee1. Een voorstel voor een notatie van definities is verwerkt in voorbeeld I. De gedefinieerde constante wordt daarin opgevoerd als bindende variabele (abstractievariabele), het definiens als applicatie-expressie.
Voorbeeld I. De eerste 19 regels van appendix 7 (bIz. 107) uit Juttings ver taling [2J, omgezet in AUT-SL. {[a,propJ[b,prop][x,aJb} [imp, [a,----J[b,-----JpropJ {[a,----J[b,----J[c,propJ[i,{b}{a}impJ[j,{c}{b}impJ[x,aJ{{x}i}j} [trimp, [a,----J[b,----J[c,----J[i,---------J[k,---------J{c}{a}impJ [con,propJ {[a,----J{con}{a}imp} [not, [a,----JpropJ {[a,----J{{a}not}not} [weI, [a,----JpropJ {[a,----J[al,aJ[x,{a}notJ{al}x} [weli, [a,----J[al,-J{a}welJ ret,
[a,----J[w,{a}welJaJ
{[a,----J[cl,conJ{[x,{a}notJcl}{a}et} [cone, [a,----J[cl,---Ja] {[a,----][b,----J[n,{a}notJ{[x,con]{x}{b}cone}{n}{b}{con}{a}trimp} [th2, [a,----][b,----][n,------J{b}{a}impJ
H
- 3 -
Opmerkina: Bovenstaande AUT-SL tekst is te lezen als een lange regel (SL staat voor single line, een enkele regel). We kunnen er een correcte AUT-SL expressie van maken door vooraan toe te voegen: [prop,primtype] en achteraan (bijvoorbeeld): primtype, waarbij we primtype beschouwen ale de constan1 te van graad 0, die in [6J 1 wordt genoemd ). Dan is prop een variabele van graad 1. De enige andere variabele van graad 1 die we hoeven te gebruiken in van AUT-QE afgeleide AUT-SL-teksten is type. In die teksten vinden we verder slechts variabelen van graad 2 en 3. (Voor een interpretatie: zie Jutting [2], bIz. 9.) 3. Constructie van een bewijs; een voorbeeld We zullen het "bewijs van th2" uit vb. I trachten te reconstrueren door aIleen naar de relevante expressies te kijken, niet naar de wiskundige inhoud of betekenis. Hiertoe zullen we voorlopig op nonnaalvormen overgaan, omdat we onderweg niet gestoord willen worden door eventueel noodzakelijke reducties. Voorbeeld I zonder het stuk dat betrekking heeft op th2 en gelezen als een enkele regel, reduceert tot de normaalvorm: [con,propJ [et,[a,propJ[w,[x,[y,aJconJconJaJ , eventueel voorafgegaan door [prop,primtypeJ. De buitenste abstractoren van deze expressie bevatten de primitieve notions, vertaald naar AUT-SL. Nu bestaat een "bewijs van th2" uit een expressie met het volgende type (in normaalvorm): [a,propJ[b,propJ[n,[x,aJcon][x,aJb • We gaan na hoe zo een expressie gevonden kan worden. Als we A E B schrijven voor "A heeft type B", is de situatie als voIgt: Gegeven: can E prop et
E [a,prop][w ,[x ,[y,aJconJcon]a
a
E prop
b
! !
n
prop [x,a]con
xo E a Gezocht: expressie E b. 1)
Joss_ties Jextra assumptie
In [6J wordt de graad geteld vanaf 1; T heeft daar graad 1; expressies van willekeurige graad n (n € m) worden in [6J toegelaten.
- 4 -
Diseussie: Een expressie X E b valt in dit geval aIleen te maken door in de "funetie" et tweemaal te applieeren, eerst met een expressieX !prop, dan met 1
een expressie X2 ! [x,[y,X1]con]eon. Dus we zoeken Xl en X2 zo dat {X 2}{X 1 }et E b. Nu geldt: {X 2 }{X 1}et! XI' dus Xl moet b zijn. Dus moet X2 E [x,[y,b]eon]con. Voeg toe aan de gegevens: x E [y,b]con, en zoek een expressie
Xi
E con. Dit
kan op drie manieren: doorinet,innofinxteappliceren.We kiezenvoorhet middelste, zoeken iets van type a (kiezen daarvoor xO) en vinden {~}n ! con. Dus X2 • [x,[y,b]con]{xO}n en {X 2 }{X l let = {[x,[y,bJconJ{xO}n}{blet, het gezochte "bewijs van th2". We noemen de laatate expressie: bewijs B.
•
Opmerkins I: Bewijs B is de normaalvorm van bewijs A, de expressie [a,----J[b,----J ••• {a}trimp uit voorbeeld I. Opmerkins 2: Door in bovenstaande discussie bij het zoeken van Xi niet in n, maar in et te appliceren, kunnen we als bewijs krijgen: {[x,[y,b]con]{[x,[y,conJconJ{~}n}{con}et}{b}et
•
Deze expressie, die we bewijs C noemen, is ongelijk san bewijs B, en bei.de staan in normaalvorm, dus bewijs B en bewijs C zijn verschillend. N.B.: Door steeds et en niet n te kiezen, komen we in een niet aflopend proces te rech t • Opmerkins 3: De inhoud van de bewijzen A, B en C kan als volgt worden voorgesteld. De drie bewijzen beginnen elk met de onderstellingen !:a:prop I, Ib:propl en la-conl, om daarna te vervolgen met: Bewijs A:
r;:on)~on :. b wegens ET •\ c oll"'l'b
Bewijs C:
Bewijs B:
}
a-con :. a-tb wegens trimp
a
a
:.con
:.con
:. (~on).-con :.b wegens ET
:. (coJ:lllt'Con)""'Con
:. a-ob
:. con wegens ET :. (b.-con)""'Con :. b wegens ET :. BI"I'b
met ET: uitgesloten derde en trimp: transitiviteit van de implicatie. Merk op dat bewijs C een "omweg" bevat.
- 5 -
4. Analyse van de bewijzen van Satz 1 en Satz 2 Satz 1 en 2 uit Juttings appendix 7 zien er ingewikkelder uit. In beide gevallen beschikken we over de volgende primitieve gesevens (afkomstig van PN's): con et
! prop ! [a,prop][w,[x,[y,aJcon]conJa
is
! [sigma,type][s,sigmaJ[t,sigmaJprop
refis! [sigma,typeJ[s,sigma]{sl{s}{sigmalis set
! [sigma,typeJtype
esti !
[sigma,type][s,~igma][sO,{sigma}setJprop
setof! [sigma,type][p,[x,sigma]propJ{sigma}set
•
estii E [sigma,typeJ[p,[x,sigma prop][s,sigma][sp,{s}pJ{{p}{sigmalsetof} {SHsigma}esti estie ! [sigma,tyPeJ[p,[x,sigma]prop][s,sigmaJ[e,{{p}{sigma}setof} {s}{sigma}estiJ{s}p nat
E type E nat
suc
! [x,nat]nat
ax3
! [x,nat][x,{l}{{x}suc}{nat}is]con
ax4
E [x,nat] [y,natJ[u,{ {y}sucH {xlsuc}'{ natHsHyHxHnatHs
ax5
! [s,{nadset][u,{sl{ I Hnadesti] [v,[x,nat][x',{s}{x}{nat}estiJ{s}{{x}suc}{nat}esti] [x,nat]{s}{xl{nat}esti.
•
Voor het bewijs van Satz 1 voegen we toe: gegevens uit assumpties: x E nat y ! nat n E [x,{y}{x}{nat}is]con. gezocht: expressie E {{ylsuc}{{x}suc}nis • Voeg daarom toe: e,xtra
[~,{{y}suc}{{x}suc}{nat}is]con.
ass~tie:
xo E {{y}suc}{{x}suc}{nat}is • gezocht: X ! con oplossins: lve zoeken X door in n te appliceren: X := {XI In. Zoek daartoe Xl E {y}{x}{nat}is. Dit doen we door in ax4 te appliceren: Xl :- {X13}{X12}{Xl l}ax4! {X 12 }{x]I}{nat}is •
- 6 -
Dus XII - x en X12 == y. Er moet gelden: XI3 E {{x I2 }suc}{{X 11 }suc}{nat}is ~ = {{y}suc}{{x}suc}{nat}is. Kies Xl3 :- XU' Dan Xl • {xO}{y}{xlax4 en de oplossing is: X ... {X1}n ... {{x }{y}{x}ax41n! con. O Dit bewijs is eenvoudig te leveren. De keuzen 4ie we gedaan hebben waren: I. We zoeken X m.b.v. n, 2. XI m.b.v. ax4,
l3 :- xo. Men kan hier verdedigen, dat deze keuzen voor de hand lagen. 3. X
~
Heel anders is de situatie bij het zoeken van het bewijs van Sa~z 2, dat een ingewikkelde structuur blijkt te hebben. De oplossing verloopt desondanks langs dezelfde lijnen als in de eerder genoemde voorbeelden. Kort weergegeven ziet die oplossing er als voIgt uit: primitieve gesevens: zie bij Satz 1. seseven uit assumptie: Xo ! nat extra assumptie: z! {xO}{{xO}suc}{nat}is sezocht: X ! con. oplossing: X := {X }{X }{X }{X }{X }estie 2) S 4 3 2 XI :- nat X := [x,X 1][y,{x}{{x}suc}{nat}is]con 2
•
X3 := Xo X4 := {X44}{X43}{X42}{X41}axS X41 := {X2 }{X 11setof X42 := {X424}{X423}{X422}{X421}estii X421 := nat X422 := X2 X 423 := I X424 := [y,{I}{{1}suc}{nat}is]{X4242}{X4241}ax33) X 4241 := 1 X4242 :- y 2) I n eerste 1nstant1e ' '" . s 1 ech ts 4 app l'lcatoren vere1st. • 0 nze Z1Jn b"1J est1e keuze X2 := [x,nat][y,{xH{x}sucHnat}is]con E [x,nat]prop maakt echter een vijfde applicator {Xs } noodzakelijk. Bij deze X2 is namelijk {X4 }{X3}{X2}{X t }estie! {X 3}X ... [y,{xO}{{xo}suc} nat is]con, waarin de 2 "extra" applicator [y,----] terugkeert. AppIicatie van Xs levert nu pas een expressie E con, als gevraagd. (Het was toegestaan om de applicator [y,----] in X2 op te nemen, omdat AUT-QE beschikt over de eigenschap: type-inclusie.)
• - 7 -
X43 :- [x,nat][x',{X41 }{x}{nat}esti]{X434}{X433}{X432}{X431}estii X := nat 431 X := X 432 2 X :- {x}suc 433 X := [y,{{x}suc}{{{x}suc}suc}{nat}is] 434 4 {X434S}{X4344}{X4343}t(4342}{X4341 }estie ) X4341 := nat X 4342 X4343 X 4344 X4345
•
:= X 2 := x := x' := {X43453}{X43452}{X43451}ax4
X43451 := {x}suc X43452 := x X43453 := y
Xs
X :- X 44 2 := z.
Opmerkins: De weg die we volgen om een oplossing te vinden introduceert twee n-expansies. Reductie hiervan Ievert een expressie die gelijk is aan de normaalvorm van het bewijs van Jutting. Bovenstaand bewijs van Satz 2 bestaat uit 28 definities van het type
•
Xa := expressie. Van deze definities zijn er 10 gedwongen, de overige 18 berusten op keuzen, De keuze die het moeilijkst Iangs mechanische weg tot stand kan komen, is die van X , Boven wordt voor X ! [x,nat]prop het predicaat 2 2 [x,nat][y,{x}{{x}suc}{nat}is]con genomen, of, anders gezegd, het predicaat x , suc(x). Het lijkt niet waarschijnlijk, dat de keuze van de extra applicator [y,----] gedaan kan wprden zonder rekening te houden met de wiskundige inhoud van Satz 2. (Tenzij men plausibel kan maken dat de extra assumptie z E xo
= suc(xO)
in deze richting wijst.) De type-inciusie lijkt hier op het
eerste gezicht een rol te spelen (zie ook voetnoot 2». Maar bij nadere beschouwing Iijken de hier gemelde moeilijkheden inherent aan inductiebewijzen en daarom niet te vermijden.
3) Met n-reductie is [y,----J{X
} te verwijderen, 4242 4) Hier is de applicator {X • Ver}nodig als gevolg van de keuze van X 4345 4342 gelijk met bovenstaande voetnoot 2).
.. - 8 -
De meeste andere keuzen zien er aanmerkelijk minder gecompliceerd uit; ze kunnen wellicht mechanisch tot stand gebracht worden bij een geschikte zoekstrategie. 5. Voorlopige conclusies De constructie van een bewijs langs de lijnen zoals hierboven aangegeven berust op een beperkt aantal heuristische regels. 5amengevat kan men deze globaal als voIgt omschrijven: 1. De uitgangssituatie is in elke fase dezelfde: de gegevens staan genoteerd
ala een rij E -formules (te beschouwen als een "telescoop", een rij ab-
•
stractoren), die volgens AUT-5L-regels zijn opgebouwd. De expressies in de gegevens staan in normaalvorm. Verder hebben we de beschikking over een expressie Y die correct is ten opzichte van de gegevens. Gezocht wordt een expressie X, .correct ten opzichte van de gegevens,met X! Y.' 2. Als Y begint met een abstractor, Y = [x,AJY', voegen we x! A aan de gegevens toe en zoeken we een X' E Y'. 3. Als Y niet met een abstractor begint, Y • {A }{A _ I } ••• {A 1}y met n ~ 0, n n dan geeft de y aan waar gezocht moet worden. Zoek in de gegevens een Eformu1e die eindigt op y, of een !-formule die eindigt op een inwendig gebonden z van dezelfde graad als y (z is inwendig gebonden in de formule p ! B als z niet vrij is in B). Zoek applicatoren die passen bij de abstractoren uit zo een E-formule. Dit komt weer neer op het zoeken van expressies X"
! Y". De typeringseisen zorgen ervoor dat sommige van die X"
a1 bij voorbaat vastliggen. Bet zal duidelijk z1Jn dat men kan-proberen om een zoekstrategie te bedenken die rekening houdt met de bovenstaande heuristische regels. Bet is een vraag hoe effectief zo een strategie kan zijn, vooral omdat terminering niet vaststaat. Bovendien kan het aantal mogelijkheden, waaruit op een bepaald moment gekozen moet worden, aanzienlijk zijn, hoewel er aan de andere kant steeds een aantal E-formules is dat zeker niet in aanmerking komt. In het voorbijgaan merken we op dat toepassing van een versie van AUT-5YNT (zie [2]), in plaats van AUT-5L, het aantal plaatsen waar gekozen meet worden zal verminderen. Problemen van wezenlijke aard, zoals gesignaleerd aan het eind van het laatste voorbeeld (de keuze van het predicaat nodig bij de inductie), lijken echter te verhinderen dat een algemeen toepasbare, practische zoekstrategie ontwikkeld kan worden. Misschien kan een strategie gebaseerd op de Bruijns
- 9 -
"nervous searching", gecombineerd met een aantal concrete aanwijzingen (hints), toch een redelijk aantal bewijzen binnen een redelijke tijd afleveren. Maar de mogelijkheid daarvan blijft op dit moment nogal speculatief. Een ander punt is, dat het niet verantwoord lijkt om steeds terug te gaan op de normaalvorm. Een groot nadeel is de lengte van de normaalvormen, een ander dat tussenresultaten, vaak onontbeerlijk bij het bedenken van een bewijs, worden genegeerd. Ret is in dit stadium nog onduidelijk, hoe de voordelen van tussentijdse definities (eventueel tot PN's verklaard) te combineren zijn met de betrekkelijke eenvoud die kenmerk blijkt te zijn van een heuristiek op basis van normaalvormen.
•
Tot slot merken we het volgende
OPe
In de boven gegeven voorbeelden van
bewijsanalyse is de nadruk gelegd op de technische kant van het proces van bewijzen, door alleen uit te gaan van de structuur van de expressies die als gegevens en als te bewijzene optreden, en niet van hun wiskundige inhoud. Ook de constructie van de ontbrekende ketting van argumenten, het bewijs, geschiedde zoveel mogelijk langs taaltechnische weg. Dit is gedaan omdat het waarschijnlijk leek dat langs deze wee een (gedeeltelijke) mechanisering van bewijzen de meeste kans op practische realisering zou hebben. Bij nader inzien verdient het wellicht de voorkeur om aansluiting te zoeken bij de wiskundige manier van denken en argumenteren, en om niet in de eerste plaats naar mechanisering van bewijzen, maar naar een algemene vorm van bewijsanalyse te streven. 6. Verwijzingen [1]
E. Landau, Grundlagen der Analysis, 3rd ed., Chelsea Publ. Comp., New York, 1960.
[2]
L.S. van Benthem Jutting, Checking Landau's "Grundlagen" in the Automath System, proefschrift Technische Rogeschool Eindhoven, maart 1977.
[3]
N.G. de Bruijn, Automath, a language for mathematics, Notes (prepared by B. Fawcett) of a series of lectures in the Seminaire de Mathematiques Superieures, Universite de Montreal, 1971.
[4]
R.P. Nederpelt, Lambda-Automath I en II, Notities Technische Rogeschool Eindhoven, afd. Wiskunde, januari en april 1971.
[5]
N.G. de Bruijn, AUT-SL, a single line version of Automath, Notitie Technische Rogeschool Eindhoven, afd. Wiskunde, mei 1971.
[6]
R.P. Nederpalt, Strong Normalization in a Typed Lambda-calculus with Lambda-structured Types, proefschrift Technische Rogeschool Eindhoven, juni 1973.
