[Programmiererstammtisch] "Zum ächzenden Compiler"

[E-Feld]

Wenn du es genau wissen wolltest, kannst du dir natürlich den generierten Maschinencode anschauen, wie sin und cos genau übersetzt wurden.

[Tiramisu]

Ist es möglich, einem Computer mathematische Beweise beizubringen, die er automatisch durchführt? Ich hab gehört, einige Leute sind dran gescheitert, aber ich halte es dennoch für möglich. Zumindest "halbautomatisch" sollte eine Software sowas doch leisten können.

[Yucatan]

i. A. nicht. Zu viele Möglichkeiten (welche Axiome? Welche Beweisidee?), alles durchzuprobieren hat eine zu große Laufzeit.

Zudem kannst du keinen Algorithmus basteln der dir zu einer Aussage und einem Beweissystem sagt, ob die Aussage in diesem System beweisbar ist (Stichwort Kollege Gödel).

Für spezielle Fälle und einer überschaubaren Wissensbasis bietet sich Prolog an. Das beruht auf dem Paradigma der Logik Programmierung.
Ansonsten müsstest du deinem Programm sagen, wie es beim Beweis vorgehen soll und wann der Beweis fertig ist

[Tiramisu]

Man bringt dem PC die Denkweise von Menschen bei. Das sollte doch gehen! Zumindest bei überschaubaren Beweisen. Einige Denkmuster kommen bei Beweisen häufiger vor.

[Allmächtig]

Ne "Induktionsmaschiene" kann ich mir gut vorstellen, dass ist einfach nur Schritt für Schritt umformen und einsetzten.
Aber wirklich allgemein Beweise erbringen können?
Das dürfte in etwa gleichbedeutend mit einer echten, kreativen(und dem Menschen mindestens gleichwertigen) KI sein.

[Tiramisu]

Gut, wenn ihr alle das so pessimistisch seht, dann versuche ich es eben selber.

[Peregrin_Tooc]

Es geht grundsätzlich schon für bestimmte Klassen von Problemen. Dafür muss man aber das Problem und die Sprache der Mathematik für den Computer übersetzen. Und Programme können nicht kreativ sein. Mit einer Art Monte-Carlo-Algorithmus könnte man aber sicher für viele Klassen von Problemen Lösungen bekommen. Ob die Beweise dann einen großen Erkenntnisgewinn liefern, glaube ich wiederum eher nicht ...

[Allmächtig]

Wer hat Ahnung von Haskell?
Ich hab trotz etwas Suchen nämlich nicht rausbekommen, wie und ob das geht, was mir hier vorschwebt:
Ich will eine function schreiben die abhängig von den Eingaben eine neue function ausgibt.

Also zum Beispiel sowas:
beispiel :: (Ord b) => a->b->(a->b)->(b->b->c)->(a->a->c)
beispiel test wert f g

Die Funktion, die ausgegeben wird(nennen wir sie mal h), soll dann so aussehen:

| f(test)>=wert "gebe aus" h(a1,a2):=g(f(a1),f(a2))
| otherwise "gebe aus" h(a1,a2):=g(f(a2),f(a1))

Mein Problem ist: Ich kenne zwar die Signatur, hab aber keine Ahnung wie ich die eigentliche funktion definiere, und wie ich eine ganze funktion ausgebe statt nur einen Wert
Ich fände es toll wenn das ginge, damit könnte ich "on the run" neue Funktionen definieren, die von den bereits erziehlten Zwischenergebnissen abhängen.

Das ursprüngliche Problem, wo mir der Gedanke, sowas zu machen, kam, habe ich jetzt schon anders gelöst. Aber die generelle Frage schwebt mir halt immer noch im Kopf herum

Hat wer Ideen?

[alpha civ]

Da gibt es mehrere Möglichkeiten.

Man kann direkt aus vorhandenen Funktionen neue Erstellen, indem man diese Funktionen nicht alle nötigen Parameter übergibt.
Hat man z.B. die Funktion

mult :: (Num a) => a -> a -> a
mult x y = x * y

dann definiert

f = mult 2

eine neue Funktion.


Andere Möglichkeit:

make_mult :: (Num a) => a -> (a -> a)
make_mult x = f
    where f y = x * y

Alternativ zu where hätte man auch let verwenden können.

Man kann dann schreiben f = make_mult 2.

[alpha civ]

Dein Beispiel kann dann in etwa so aussehen:

beispiel :: (Ord b) => a->b->(a->b)->(b->b->c)->(a->a->c)
beispiel test wert f g = if (f test) >= wert
                         then h1
                         else h2
    where h1 x y = g (f x) (f y)
          h2 x y = g (f y) (f x)

[Allmächtig]

Cool danke

[Gullix]

Ist es möglich, einem Computer mathematische Beweise beizubringen, die er automatisch durchführt? Ich hab gehört, einige Leute sind dran gescheitert, aber ich halte es dennoch für möglich. Zumindest "halbautomatisch" sollte eine Software sowas doch leisten können.

...also, prinzipiell ist das möglich. Mathematische Aussagen kann man ja als Zeichenkette aufschreiben, mit Quantoren. Und man kann eine Liste aller erlaubten Veränderungen dieser Zeichenketten aufstellen, zum Beispiel "A => B umwandeln zu nichtB => nichtA". Dann kann man die Axiome in diesen Zeichenketten ausdrücken und mit irgendeinem Algorithmus den Graphen erkunden. So erreicht man alle beweisbaren Aussagen, wenn man nur lange genug wartet und die ganzen nebenbei produzierten Unsinnsaussagen aussortiert.

In der Praxis stößt man da aber auf eine Menge Probleme. Der Computer kann kaum erkennen, wenn er in die falsche Richtung abbiegt. Man erhält sehr viele Aussagen, die trivial sind oder die man einfacher formulieren könnte, und die kann man kaum automatisiert aussortieren. Und vor allem wird die Anzahl der Aussagen wahnsinnig schnell größer, weil halt so unfassbar viele Aussagen beweisbar sind.

Was man eher macht, ist ganz bestimmte Teile von Beweisen automatisieren. Der Vierfarbensatz (jede 2d-Landkarte kann man mit vier Farben so einfärben, dass angrenzende Länder nicht die gleiche Farben haben) ist ein Beispiel, kannste ja mal googlen und dir das Paper dazu durchlesen.

[Tiramisu]

Niemand versteht mich!
Bei vielen Beweisen kommen immer wieder dieselben Beweis-Ideen bzw. Beweis-Motivationen vor. Wenn der Rechner solche Dinge können würde, wäre ich fürs Erste zufrieden. Das ist doch wirklich nicht zu viel verlangt.

[Slaan]

Programmiers doch

[Tiramisu]

Bin grad dabei.
Solche Visionäre wie ich werden anfangs immer verpönt, aber wartet es nur ab!