Game semantics - The full abstraction problem for PCF

Abstract

Spielsemantik basiert auf dem Formalismus der dialogischen Logik. Sie war ursprünglich eine Möglichkeit um die Semantik von intuitionistischer Logik und linearer Logik zu definieren. Wenig später erwies sich Spielsemantik als äußerst nützliches Werkzeug zur Interpretation verschiedener Programmiersprachen. Spielsemantik modelliert ein Spiel zwischen einem Spieler und Gegenspieler, der erstere repräsentiert das Programm selbst und der letztere den Kontext des Programms. Das Ziel dieses Modells einer Programmiersprache ist das formale Schließen über Programmiersätze, um unter anderem Compiler Optimierungen zu verbessern. Diese Arbeit ist, wie auch die meiste Literatur, hauptsächlich auf die funktionale Programmiersprache PCF fokussiert. Es werden einige vielversprechende Ansätze vorgestellt, die nicht auf Spielsemantik basieren und die das Problem der vollständigen Abstraktion nicht zufriedenstellend lösen konnten. Schließlich wird Spielsemantik und deren Anwendung auf PCF erklärt. Außerdem wird ein Ansatz auf dem aktuellen Stand der Entwicklung vorgestellt, der es ermöglicht Programmiersprachen mit Nebenläufigkeit und Wahrscheinlichkeiten zu interpretieren. Diese Arbeit stellt eine Einführung in das Thema der Spielsemantik und der Interpretation von PCF dar. Mathematische Konzepte die in anderen Publikationen implizit vorausgesetzt sind, werden hier detailliert erklärt.

Game semantics, a formalism based on diaogue games used in semantics of intuitionistic logic and later linear logic, have proven to be quite useful in the interpretation of programming languages. They model a play between a player and an opponent, one regarded as the program context and the other as the program itself. The aim of creating such a model is being able to reason about equality of program phrases, in order to improve compiler optimization amongst other applications. This thesis focuses on the interpretation of the programming language PCF. From the first models based on complete partial orders, to models introducing sequentiality, and finally game semantics, which solve the major problem of full abstraction. Furthermore, we show a current state of the art approach, that extends PCF with probability and provides a fully abstract concurrent game semantics model. The thesis is aimed at readers with a computer science background familiarizing themselves with semantics of programming languages. It is self-contained, as mathematical backgrounds are explained on which the theory is built on.