Höhere Programmiersprachen, insbesondere rein funktionale mit Bedarfsauswertung, befreien den Programmierer von der Pflicht, sich darüber Gedanken zu machen, wie ihr Programm tatsächlich auf der Maschine ausgeführt werden wird. Ebenso hat der Compiler beim Optimieren von Programmen in solchen Sprachen größeren Spielraum. Dieser Abstand zur Maschine macht es allerdings auch schwieriger, vorherzusagen, wie sich die Programmtransformationen des Compilers auf die Leistung des Programms auswirkt. Daher werden solche Transformationen oft nur empirisch untersucht, indem die Leistung von ein paar wenigen Beispielprogrammen gemessen wird. So werden zwar durchaus wertvolle Anhaltspunkte gewonnen, jedoch keine allgemein gültigen Aussagen.

Formale Semantiken von Programmiersprachen können als Leitplanken bei der Implementierung eines Compilers dienen, und formale Beweise können allgemeingültig zeigen, dass ein Compiler die Bedeutung eines Programmes nicht unbeabsichtigt verändert. Können wir mit ihrer Hilfe auch beweisen, dass eine Programmtransformation, wie sie der Compiler vornimmt, in der Tat eine Optimierung ist?

Dieser Frage gehe ich in dieser Arbeit in drei Schritte nach: Ich entwickle eine neue Compiler-Transformation; ich baue die Werkzeuge um sie in einem interaktiven Theorembeweiser zu untersuchen; letztendlich beweise ich, dass das umgeschriebene Programm -- in einem geeigneten abstrakten Sinne -- mindestens so performant ist als zuvor.

\medskip

Meine Compiler-Transformation, genannt \emph{Call Arity}, wird inzwischen mit dem Haskell-Compiler GHC ausgeliefert und löst ein schon lange bestehendes Problem mit der Programmtransformation \emph{list-fusion}: Funktionen wie \hi{foldl} und \hi{sum}, die Listen verarbeiten und dabei einen Akkumulator verwenden, haben, wenn auch sie von \emph{list-fusion} umgeschrieben würden, zu unerwünscht langsamen Code geführt. \emph{Call Arity} ermöglicht es dem Compiler, solchen Code weiter umzuschreiben und wieder in eine effiziente Form zu bringen, in dem er Funktionsdefinition geeignet eta-expandiert. Die dabei entscheidende Zutat ist eine neue Kardinalitäts-Analyse, die erkennen kann, wenn eine Variable höchstens einmal verwendet wird -- und das sogar bei rekursivem Code.

Ich zeige empirisch, dass meine Analyse tatsächlich das Problem löst und nun auch in diesen Fällen \emph{list-fusion} die Leistung der Programme signifikant verbessern kann. Ich zeige auch, dass es Situationen jenseits von \emph{list-fusion} gibt, in denen meine Transformation anspringt und zu Verbesserungen führt.
%Kein Programm des Benchmarks hat durch meine Transformation Leistung eingebüßt.

\medskip

Um diese Aussagen auch formal überprüfen zu können, formalisiere ich Launchburys Semantik für Sprachen mit Bedarfsauswertung im interaktiven Theorembeweiser Isabelle. Diese verbreitete und allgemein akzeptierte Semantik modelliert Bedarfsauswertung im Lambda-Kalkül mit wechselseitiger Rekursion und ist daher in meinem Fall die Semantik der Wahl.

Um die Problematik von Namen und Bindungen, die generell eine der Hauptschwierigkeiten bei der Formalisierung von Programmiersprachen ist, in den Griff zu bekommen, verwende ich Nominallogik, die für Isabelle im Paket \isa{Nominal2} implementiert ist. Meine Formalisierung ist eine der größten Isabelle-Formalisierungen, die \isa{Nominal2} verwendet, und die erste, die es effektiv mit dem \isa{HOLCF}-Paket, welches Domänentheorie umsetzt, kombiniert. Mein erster Anlauf, diese Techniken zu kombinieren, scheiterte; ich erkläre, wie und warum, und beschreibe, wie ich die Probleme letztendlich überwand.

Darüber hinaus habe ich den ersten rigorosen Beweis, dass Launchburys Semantik adäquat ist, geführt. Launchburys Beweisansatz widersteht bisher jeglichen Versuchen, ihn zu vervollständigen. Ich wich ein wenig von dem Weg ab, den er umrissen hat, und fand so einen eleganteren und direkteren Beweis.

\medskip

\goodbreak

Auf dieser Formalisierung baue ich auf, modelliere die \emph{Call Arity}"=Transformation und -Analyse in Isabelle und beweise, dass sie die Leistung der Programme nicht verringert. Als abstraktes Leistungsmaß verwende ich dabei die Anzahl der Speicherzellen, die das Programm anfordert. Ich erkläre, warum dies in meinem Fall eine geeignete Wahl ist. Der Beweis ist modular und führt das Konzept der \emph{trace trees} ein, mit der sich abstrakte Kardinalitäts-Analysen beschreiben lassen.

Bei jeder Formalisierung, ob Computer-geprüft oder nicht, entsteht ein Formalisierungs-Spalt zwischen dem Modell und dem Modellierten. Ich bemesse die Breite des Spaltes, der sich im vorliegenden Fall insbesondere daraus ergibt, dass \emph{Call Arity} nur ein Teil eines großen, produktiv eingesetzten Compilers ist.

\medskip

Insgesamt führe ich also eine neue Programmanalyse ein, die ein offenes Problem mit \emph{list fusion} löst und auch darüber hinaus den Compiler verbessert. Darüber hinaus zeige ich, wie formale Methoden genutzt werden können um auf dieser hohen Abstraktionsebene Beweise über nicht-funktionale Eigenschaften wie das Performanceverhalten zu führen.
