Praktische Informatik I - mathematik.uni-marburg.degumm/Lehre/WS08/BB/0 Geschichte.pdf · © H....

Berechenbarkeit, Beweisbarkeit

Geschichte

© H. Peter Gumm, Philipps-Universität Marburg

Inhalt

1. Wahrheit ausrechnen – der Traum 1. Aristoteles 2. Lullus3. Leibniz

2. Entwicklung der Grundlagen1. Boole 2. Frege 3. Cantor4. Russel

3. Grenzen des Berechnens, 1. Hilbert2. Turing 3. Gödel 4. Davis, Matiyasevitch, Putnam

4. Logik und Berechnung1. Schönfinkel2. Church3. Curry4. Robinson, Kowalski, Colmerauer


Aristoteles

n Syllogismen¨ Terme¨ Propositionen¨ Schlussfiguren Aristoteles

384-322 B.C.

A, A ) B

B

modus ponens

A ) B, : B,

: A

modus tollens

Alle Menschen sind sterblichSokrates ist ein Mensch

Sokrates ist sterblich

Heutige Sichtweise:


Der Traum des Raymundus Lullus

Raymundus Lullus 1233-1315

Ars Magna, Ars combinatorica

Experimente mit mechanischen Hilfsmitteln

um Aussagen zu finden, zu kombinieren und

zu beweisen.

Übte grossen Einfluss auf G.W.Leibniz

(1646) aus.

Wollte alles was in der Bibel steht beweisen.


Leibniz

n Erfindet Binärsystemn Konstruiert Rechenmaschinen Erster Logikkalküln Gleichungslogik

x = y, y = z

x = z

x1 = y1 , … , xn = yn

f(x1,…,xn) = f(y1,…,yn)

x = y

y = xx = x

Leibniz-Regel = ist Äquivalenzrelation

Gottfried Wilhelm Leibniz 1646-1716

Traum (Calculus ratiocionator): Jedem Begriff wird eine Zahl zugeordnet.

Durch Kombination kann Wahrheitsgehalt jeder Aussage ausgerechnet werden.


Boolesche Algebra

n George Boole: Algebra der Logik

n Verknüpfung elementarer Aussagen zu einer komplexen Aussage

¨ Wahrheitsgehalt der gesamten Aussage errechnet sich aus den Wahrheitsgehalten der Teilaussagen

n A = es regnet, n B = die Straße ist nass,n C = (A ) B)

n AÆ C = A Æ (A ) B) = A Æ (:A Ç B) = (A Æ :A) Ç (A Æ B) = 0 Ç (A Æ B) = (A Æ B).

Folglich: Wenn A wahr ist und A ) B wahr ist, errechnet sich B zu wahr.

George Boole

1815-1864


Quantorenlogik

n Boolesche Logik ist zu abstrakt

n Elementare Aussagen in der Mathematik müssen weiter analysiert werden¨ Aussagen über

n Beziehungen von Elementen untereinandern Werte von Funktionen

¨ Quantifizierte Aussagenn 8 x. P(x)n 9 x. P(x)

n Beispiele: ¨ gerade(x) := 9 y. y+y=x¨ prim(x) := 8 y1.8y2. 1 · y1 + y2 Æ y1+y2 < x ) :(y1*y2=x) ¨ 8 x. gerade(x) ) 9 y1. 9 y2. prim(y1)Æ prim(y2)Æ y1+y2=x.

Gottlob Frege

1848-1925

Erfindet:

Quantoren 8, 9


Endliche und unendliche Mengenn Entwickelt die (naive) Mengenlehre

n Entwickelt Kardinalitäten und Arithmetik unendlicher Mengen

¨ Zu jeder Kardinalzahl gibt es eine nächst-größere …

¨ 0 = { }, 1 = { 0 }, 2 = { 0, 1 }, …., n+1 = { 0, 1, … , n }, … ,

¨ @0 = |N| , nächste: @1 , nächste @2, …

n Diagonalargument

¨ Für keine Menge X gibt es eine surjektive Funktion

f: X ! P(X)

n |X| < |P(X)| < |P(P(X) )| < …

n R hat mehr Elemente als N also @1 · R

n Kontinuumshypothese : R = @1 ?

Georg Cantor

1845-1918


Das Problem des Barbiers

n Axiomatisierung der Zahlentheorie¨ unabhängig auch Frege

n entdeckt Antinomien der „naiven“ Mengenlehre

¨ R := { x | x ∉ x } darf keine Menge sein

n Lösung: ¨ Typentheorie ¨ Wurzel getypter Programmiersprachen

Populärversion:

In in einem Ort gibt es einen Barbier, der behauptet, er rasierealle Männer in dem Ort, nur nicht die, die sich selbst rasieren.

Was macht er dann mit sich selbst?

Rasiert er sich selbst ) er darf sich nicht rasieren

rasiert er sich nicht selbst ) er muss sich rasieren


Hilberts Präzisierung von Leibniz‘ Traum

David Hilbert 1862-1943

Syntax

zahlentheoretischer Aussagen:

Variablen

v → x | y | z | ...

Terme:

t → v | 0 | t+1 | t1+ t

2| t

1* t

2

Ausdrücke:

e → t1= t

2| t

1< t

2

| e1

∧ e2 | e

1 ∨ e

2 | ¬ e

| ∃ x.e | ∀ x.e

Aussagen:

Ausdrücke ohne freie Variablen

Finde eine Methode, zu einer

beliebigen zahlentheoretischen

Aussage zu entscheiden, ob

sie wahr ist oder falsch.


Bescheidenere mathematische Träume

10. Hilbertsches Problem (1900) :

Finde eine allgemeine Methode um diophantische Gleichungen zu lösen.

Eine diophantische Gleichung ist ein Ausdruckp(x1, ... , xn) = 0

wobei p ein Polynom mit ganzzahligen Koeffizienten ist. Eine Lösung ist eine Folge a1, ... an von ganzen Zahlen mit p(a1, ... , an) = 0.

Beispiele:

4x - 2y – 3 = 0 hat keine Lösung4x - y - 3 = 0 hat unendlich viele Lösungen x2 + y2 - z2 = 0 hat unendlich viele Lösungen

Finde eine allgemeine Methode um zu entscheiden, ob eine gegebene diophantische Gleichung eine Lösung hat

http://aleph0.clarku.edu/~djoyce/hilbert/problems.html

David Hilbert 1862-1943


Was ist eine „Methode“ ?Alan Turing (1912-1954)

Präzisiert

Allgemeine Methode = Algorithmus

durch

Turing-Maschine

Turing-Maschine: extrem einfaches mathematisches Maschinenkonzept

Viele alternative Definitionen für „Methode“ bzw. „Algorithmus“

wurden versucht. Alle stellten sich als „äquivalent“ zur Turing-

Maschine heraus.

Turing zeigt, dass es Berechnungsprobleme gibt, die algorithmisch nicht lösbar sind.


Leibniz‘ Traum ist unerfüllbar

Kurt Gödel 1906-1978

Es gibt keine „Methode“, um die Wahrheit eines

beliebigen Satzes der Zahlentheorie zu berechnen.

Es gibt kein „Axiomensystem“ aus dem mit der

Quantorenlogik genau die wahren Aussagen der

Zahlentheorie hergeleitet werden können.

Wenn Σ ein Axiomensystem für die Zahlentheorie ist, dann gibt es zwei Möglichkeiten :

− Σ ist inkonsistent, d.h. aus Σ folgen auch unwahre Aussagen, oder

− Σ ist zu schwach, d.h. es gibt wahre Aussagen, die nicht aus Σhergeleitet werden können.


Hilberts 10. Problem ist unlösbarWichtige Vorarbeiten zum Beweis dieser Behauptung

stammen von den Logikern/Philosophen

Julia B. Robinson 1919-1985

Viele spannend zu lesende Artikel und Bücher von Martin Davis, insbesondere:

*Neu* Buch: M.Davis: Engines of Logic. (Semesterapparat) *Neu*

Artikel: M.Davis:What is a computation

in dem Buch Mathematics today (Semesterapparat)

Martin Davis* 1928 www.cs.nyu.edu/cs/faculty/davism/

Hilary Putnam* 1926


Yuri Matiasevitch erledigt Hilberts 10. Problem

Es gibt keine allgemeingültige Methode

um zu entscheiden, ob eine vorgelegte

Diophantische Gleichung eine Lösung hat.

Yuri bewies dies 1970

(im zarten Alter von 22)

in seiner Doktorarbeit.

[email protected] Fragen ?

http://logic.pdmi.ras.ru/~yumat/Homepage:

Yuri Matiyasevitch

* 1947


FunktionenkalkülAlonzo Church

1903-1995

Entwickelt einen „Kalkül für Funktionen“,

heute „Lambda-Kalkül“ genannt..

- Basis aller funktionalen Sprachen

Datenstruktur für Funktionen f

Methoden:Anwendung : apply(f,a) Konstruktor : abstract(x,e)

Konventionelle mathematische Notation:

f(a) statt apply(f,a)x a e statt abstract(x,e)

Church‘s Lambda-Notation:f a Anwendung von f auf aλ x.e Abstraktion

Beispiel: square := λx. x * xsquare 3 = 9

f:N!N ist λ-definierbar , f ist Turing-berechenbar


Kombinatorische Logik

Moses Schönfinkel 1889-1942

Entwickelt einen variablenfreien

Kalkül für Funktionen

Aus den Grundfunktionen

S, K und I, mit

I x := x

( K x) y := x

((S x) y) z := (x y)(x z)

können alle berechenbaren

Funktionen konstruiert werden.

n-stellige Funktionen können auf 1-stellige zurückgeführt werden: Die Funktionen

f : A × B → Centsprechen ein-eindeutig den Funktionen

fc : A → ( B → C ). Das nennt man heute „currying“


Curry-Howard-Isomorphismus

n Lambda Kalkül und kombinatorische Logik

¨ Lambda-Term t hat Typ α, α ist logische Aussage und t ihr intutionistischer Beweis

n Beispiele:¨ λx.x hat Typ α! α und p ! p ist logisch wahr

¨ p → ( q → p ) ist wahr, λ x.λy. x hat Typ α→ (β→ α)

¨ (p → q → r) → (p → q) → p → r ist wahr,

n der Beweis ist das Programm S=λ x.λ y.λ z. (xy)(yz) n es hat Typ (α→ β → γ) → (α→ β) → α→ γ

Haskell Curry

1900-1982

Programmieren = konstruktiv Beweisen

• Programme sind konstruktive Beweise

• konstruktive Beweise sind Programme

• Program extraction


Programmieren mit Logik

n Gödel:¨ berechenbar $ arithmetisch definierbar

n John Alan Robinson ¨ Unifikation

n Bob Kowalski¨ Prozedurale Interpretation

von Implikationen (Horn-Klauseln)

n Alain Colmerauer¨ Prolog – Programmiersprache auf

Basis von Horn Klauseln

Praktische Informatik I - mathematik.uni-marburg.degumm/Lehre/WS08/BB/0 Geschichte.pdf · © H....

Documents

Transcript of Praktische Informatik I - mathematik.uni-marburg.degumm/Lehre/WS08/BB/0 Geschichte.pdf · © H....