An algebraic method for specifying regular and semantic data structures including complete binary trees, sorted lists, square matrices, powerlists, is proposed. It is shown that this method generalizes the equational approach to specifying data types. The specification method allows constructors of a data type to be partial in the sense that their behavior may be meaningful only on a subset of syntactically specified input domain. Equational and inductive reasoning techniques based on rewrite rules can be generalized to exploit this information about constructors. The use and effectiveness of this approach are illustrated with parallel algorithms and hardware circuit descriptions using Misra's powerlists. Properties of such algorithms can be verified using the theorem prover Rewrite Rule Laboratory (RRL). Machine proofs generated preserve the clarity and succinctness, to a large extent, of a hand proof.
Fortsetzung vom 29.5. Neueinsteiger willkommen !
Fortsetzung voraussichtlich am 17.7.
Structural properties of type theory, such as weakening and substitution, are traditionally verified individually by induction on derivations. In this talk we present a simple model construction that allows most of the interesting structural properties to be shown at once.
First, we briefly introduce a simple functional language "foetus" (lambda calculus with tupels, constructors and pattern matching), for which we have implemented a termination checker.
This checker tries to find a well-founded structural order on the parameters for a given function. The components of the check algorithm are: function call extraction out of the program text, call graph completion and finding a lexical order for the function parameters.
We hope to be able to demonstrate "foetus" in action using a video beamer.
A draft version of the description can be found here.
Wie schon im Februar besprochen, wenden wir uns nun Loader's Papier zu, in dem er eine Form des Kreisel-Lacombe-Schönfield Theorems benutzt, um zu zeigen, daß das PER Modell für einen lambda-Kalkül mit strikt positiven Typen voll abstrakt ist.
Besonders interessant ist, daß die Frage, ob das PER Modell für System F voll abstrakt ist, noch offen ist. Eine andere (bescheidenere) Frage ist, ob sich Loader's Resultat auch mit Ulrich Berger's Ansatz beweisen läßt.
Es ist empfehlenswert, vorher einen Blick auf das Papier zu werfen.
Der Vortrag wird voraussichtlich am 25.6. fortgesetzt.
We show how extensible records with structural subtyping can be represented directly in Church's Simple Type Theory (also known as HOL). Exploiting some specific properties of HOL, in particular the Isabelle/HOL dialect, this encoding turns out to be extremely simple. Structural subtyping is subsumed by naive parametric polymorphism, while overridable generic functions ('methods' in object-oriented parlance) may be based on ordinary overloading.
This talk aims at giving an understanding of *why* record subtyping actually works in HOL. We will point out special features (peculiarities?) of HOL that are absent in other type theories. We will also hint at the general lessons learned from this example of doing applied logic in the context of a real working environment like Isabelle.
Wolfgang Naraschewski and Markus Wenzel. Object-Oriented Verification based on Record Subtyping in Higher-Order Logic. To appear on TPHOLs'98.Wie versprochen, wollen wir Fragen und Ideen, die zu Uli Berger's Vortrag am 6.2. aufgetaucht sind, diskutieren
Uli kann den Satz, daß die Elemente von Realizability Modellen genau die totalen Elemente des Domainmodells sind, erläutern.
Als Fortsetzung schlage ich vor gemeinsam Ralph Loader's Papier Equational Theories for Inductive Types zu lesen und zu verstehen. Loader zeigt hier eine interessante Anwendung eines (etwas anderen) Totalitätsbegriffs: Für strikt positive induktive Typen ist die Theorie des PER Modells minimal. Die Erweiterung für System F steht noch aus.
Ich werde an zwei Beispielen zeigen, wie man aus konstruktiven Adäquatheitsresultaten (= Korrektheit + Vollständigkeit) Normalisierungsresultate ablesen kann:
1. ist Folklore, 2. vermutlich weniger bekannt. Die Erweiterung für die Prädikatenlogik scheint unproblematisch. Um Entscheidbarkeitsresultate für Lambda-Kalküle abzuleiten, ist die Verwendung von kategoriellen Modellen sinnvoll (nämlich Prägarben, bzw. Garben): Für 1. wurde das in unserem CTCS-Artikel getan, 2. ist noch in Arbeit.
Die Bereichstheorie nach Scott und Ershov erm"oglicht einen eleganten
Zugang zu einer konstruktiven mengentheoretischen Modellierung von
Funktionalen h"oheren Typs. Man definiert zun"achst Bereiche von
partiellen Funktionalen, um daraus dann die totalen Funktionale, an
denen man eigentlich interessiert ist, auszusondern. Diese totalen
Objekte besitzen gewisse ordnungstheoretische bzw. topologische
Eigenschaften (Dichtheit, Codichtheit), mit deren Hilfe man zum
Beispiel ein konstruktives Auswahlprinzip sowie die Isomorphie zu
Beesons Realisierbarkeitsmodell zeigen kann. Der Nachweis dieser
Eigenschaften gelingt mittels einer Verallgemeinerung des
Dichtheitssatz von Kleene und Kreisel, der besagt, dass die "ublichen
Typkonstruktoren x, ->, Pi und Sigma, aber auch Universums- und
Superuniversumsoperatoren die Dichtheit und die Codichtheit vererben.
Im Vortrag werde ich die Definitionen von Dichtheit und Codichtheit
insbesondere f"ur abh"angige Typen erl"autern und den Beweis des
Satzes skizzieren.
Adding coproducts to lambda calculus destroys the subformula property
for normal forms w.r.t. beta reduction. This problem may be
operationally resolved by adding permutative conversions.
The aim of this talk is to convince the audience that adding
permutative conversions to a lambda calculus with coproducts
(i.e. sums of types) does preserve strong normalization. The proof
will be shown for the simplest case where only arrow and sum types are
assumed to be present in the system. Felix Joachimski has given a
proof for this system back in 1995 which rests on this restriction.
In contrast to this the proof to be presented is modular in the sense
that a proof by the computability predicate method due to Tait only
has to be adjusted by some minor changes in the definition of
candidates (i.e. saturated sets). They only necessitate local changes
in the reasoning and hence allow for a much richer set of type
constructs to be studied (e.g. universal and existential
quantification and inductive types) without having to rework the proof
parts covering those extensions.
The talk is also intended to advocate the use of (general) inductive
definitions for constructing normalization proofs.
We propose to use modal logic as a logic for coalgebras and discuss it in
view of the work done on coalgebras as a semantics of object-oriented
programming. Two approaches are taken: First, standard concepts of modal
logic are applied to coalgebras. For a certain kind of functor it is shown
that the logic exactly captures the notion of bisimulation and a complete
calculus is given. Second, we discuss the relationship of this approach with
coalgebraic logic.
Dieser Vortrag besch"aftigt sich mit interaktiver Beweisf"uhrung in Typentheorien und mit Methoden, Beweise in bestimmten Fragmenten zu automatisieren. H"aufig werden beim Beweisen in Typentheorie als Platzhalter f"ur zu konstruierende Objekte Metavariablen eingef"uhrt. Es ist fraglich, wie Termoperationen wie Substitution und Reduktion in einem Kalk"ul mit Metavariablen zu definieren sind. Die Probleme eines naiven Ansatzes werden diskutiert, zu ihrer L"osung wird ein Kalk"ul mit expliziten Substitutionen vorgeschlagen und dessen Eigenschaften werden analysiert. Ein derartiger Kalk"ul eignet sich zur interaktiven Beweisf"uhrung. Es soll weiterhin untersucht werden, wie Beweissuche in (Fragmenten der) Typentheorie durchgef"uhrt werden kann und wie bestimmte Anforderungen (z.B. Variablenbedingungen in einem Sequenzen-Kalk"ul) in diesem Rahmen interpretiert werden k"onnen. Abschlie"send wird das Typelab-System vorgestellt, in dem einige der vorgeschlagenen Konzepte implementiert sind.
Es geht insbesondere darum, die Beweise von
- Haupttypisierungen im Curry-Hindley Kalk"ul ~=~ allgemeinste Unifikatoren
- Haupttypisierungen im Damas-Milner Kalk"ul ~=~ allgemeinste ??
- Haupttypisierungen im Milner-Mycroft Kalk"ul ~=~ allgem. Semiunifikatoren
- ?? bei Milner-Mycroft + polym. Abstraktion ~=~ allgem. Semiunifikatoren
zu diskutieren/vergleichen und zu vereinheitlichen.
The main aim of the project is to be able to take a mathematics book and, with a minimum of human interaction, produce correct programs from the proofs in the book. There are two aspects:1. technical and 2. psychological. For the technical aspect we use a typed lambda calculus and the Curry-Howard correspondence to code proofs. For the psychological one we are interested in how people construct proofs. (The project is not interested in theorem-proving as such: we assume that we already have some sort of proof. The questions are more about we get the machine to comprehend the proof.)
ML< erweitert das klassische ML- (Hindley-Milner-) Typsystem um eine partielle
Ordnung auf atomaren Typen. Im allgemeinen hat ein ML<-Typ die Gestalt
\forall v1...vn : k . m
fuer Variablen vi, eine Konjunktion k von Ungleichungen zwischen Monotypen
("constraint") und einem Monotyp m. Damit eignet sich ML< gut als Typsystem
fuer (funktionale) objektorientierte Sprachen, die parametrische Polymorphie a
la ML und dynamische Bindung (Polymorphie im objektorientierten Sinn) mischen.
Im Gegensatz zu ML ist die Aequivalenz zweier ML<-Typen nicht auf alpha-
Konvertierbarkeit zurueckzufuehren. Wir fuehren daher eine "semantisch"
motivierte partielle Ordnung (und Aequivalenz) auf Typen ein und formalisieren
diese durch eine geeignete Implikation von constraints.
Im Vortrag wird neben dem reinen Typsystem exemplarisch seine Anwendung auf
eine explizit getypte Sprache beschrieben, die wie CLOS oder Cecil auf
(hoeherstufigen) Multimethoden basiert, d.h. die dynamische Bindung bezieht
sich nicht nur auf ein ausgezeichnetes Empfaengerobjekt, sondern
beruecksichtigt alle Argumente. (Damit erhaelt man eine natuerliche
Verallgemeinerung sowohl funktionaler als auch objektorientierter Konzepte.)
Im Gegensatz zu der in der Literatur gebraeuchlicheren Codierung von Objekten
als records geben wir eine Interpretation von ML-Datentypdeklarationen als
Deklarationen von (abstrakten und konkreten) Objektklassen und von pattern
matching als dynamischer Bindung. Da Typen nur die Schnittstelle von Objekten
beschreiben, werden Implementierungsaspekte wie Vererbung und Verkapselung
nicht im Typsystem beschrieben, was existentielle bzw. rekursive Typen
ueberfluessig macht, sondern durch ein klassisches Modulsystem gewaehrleistet.
Es wird eine beweistheoretische Reduktion der klassischen Theorie ID^c_\nu
(\nu<\omega) auf eine konstruktiv akzeptable Theorie ID^i_\nu({\cal A})
mit strikt-positiver Definitionsklausel {\cal A} gegeben.
Als Korollar erh\"alt man, dass in ID^i_\nu({\cal A}) dieselben
rekursiven Funktionen beweisbar total sind, wie in ID^c_\nu.
Spezielle Hilfsmittel bei der Reduktion sind eine besondere
Realisierbarkeitsinterpretation, sowie eine infinit"are
Schlussregel (\Omega_{\mu+1}) mit (in gewissem Sinn) "uberabz"ahlbar
vielen Pr"amissen.
Folien
Using a canonical $\eta$-expansion-function the problem of strong
normalisation and confluence of combined $\beta$-reduction and
$\eta$-expansion is reduced to strong normalisation and confluence of
the $\lambda$-calculus with $\beta$-reduction only. The universality
of the method is demonstrated by applying it to
\begin{itemize}
\item A simply typed $\lambda$-calculus with surjective pairing and sum
types. To provide the premise of the method we also give an improved
strong normalisation proof for $\beta$ plus permutative conversions that
also allows to treat $\eta$-contractions elegantly.
\item Arbitrary singly-sorted $\beta$-strongly-normalising pure type
systems, including the systems $\FFF$, $\FFF^{\omega}$ and the
calculus of constructions.
\end{itemize}
Folien
In Martin-Loef's intensionaler Typentheorie (ITT) unterscheidet man zwischen der entscheidbaren *Urteilsgleichheit* und der unentscheidbaren, beweisbeduerftigen *propositionalen Gleichheit* ausgedrueckt durch den Identitaetstyp. So hat man z.B. in ITT die Urteilsgleichheit 1+3 = 2+2, und damit auch refl : Id(1+3,2+2), weil refl : Id(1+3,1+3) und Id(1+3,1+3)=Id(1+3,2+2). Auf der anderen Seite gilt z.B. nicht (x+y)(x-y)=x^2+y^2, wohl aber kann man (unter Verwendung des Rekursionsoperators) Term t(x,y) konstruieren, mit t(x,y) : Id((x+y)(x-y) , x^2+y^2) In der extensionalen Typentheorie (ETT) hat man nun die *Gleichheitsreflexionsregel*, welche es gestattet, aus p:Id(t1,t2) fuer ein p schon t1=t2 zu folgern. Dadurch wird die Urteilsgleichheit unentscheidbar; der (moeglicherweise komplizierte) Beweisterm p faellt ja weg. Dies zieht aber auch die Unentscheidbarkeit aller anderen Urteile, wie Typisierung und Typ-heit nach sich. Im Vortrag moechte ich zeigen, dass die Gleichheitsreflexionsregel konservativ ist ueber einer Erweiterung von ITT um zwei natuerliche Axiome. Ich werde auch moegliche Anwendungen dieses Resultats auf computerunterstuetztes Beweisen in ITT diskutieren. Der groesste Teil des Vortrages stuetzt sich auf meinen Artikel.Ich hoffe allerdings, dass es mir bis zum 31.1. gelungen sein wird, das Resultat auf eine Praesentierung von ITT mit Hilfe eines "logical framework" zu erweitern und damit ein in op. cit. offen gelassenes Problem zu loesen.
Vom 15.12.-19.12.96 fand in Aussois der erste jährliche workshop der TYPES working group statt. Thorsten Altenkirch, Bernhard Reus und Wolfgang Naraschewski (evtl.) werden darüber berichten ( Programm des workshops (vorläufige Version) ).
Außerdem wollen wir die Ergebnisse der brainstorming session in konkrete Planung umsetzen.
MuTTI = Munich Type Theory Implementation ist eine experimentelle Implementation von Typtheorie am Lehrstuhl Clote. Das MuTTI System basiert auf der Sicht von Typtheorie als funktionaler Programmiersprache und realisiert einige Idee aus gemeinsamer Arbeit mit Thierry Coquand.
Für das nächste Treffen ist kein Thema festgelegt und ich habe vor eine "Open Problem Session" zu machen, wo jeder etwas über seine gegenwärtigen (oder zukünftigen) Interessen erzählen kann. Dabei werden wir hoffentlich auch einige Themen identifizieren, mit denen sich der Club in der nächsten Zukunft (also ab Anfang '97) beschäftigen soll.
Resultate des BrainstormingsEs wird eine Erweiterung der SML-Typisierung um polymorphe Rekursion vorgestellt. Diese 'ML+'-Typisierbarkeit umfasst ML-Typisierbarkeit echt, sowohl was die Menge der typisierbaren Terme als auch was die Allgemeinheit der Haupttypen angeht. Dass sie im allgemeinen unentscheidbar ist, macht sich praktisch (bisher) nicht bemerkbar.
Bei der Typisierung mit ML+ besteht -im Unterschied zu ML- das Problem, die Quantorenstruktur von Typen (auch in den Annahmen!) zu finden. Das kann man entweder im Curry/Hindley-Stil durch Aufstellen und Loesen geeigneter (nicht lokaler) TypUNgleichungen zu einem Term erreichen, oder im sequentiellen Milner-Stil, mit Spezialisierung von Teilherleitungen (wie fuer ML in SML-Compilern ueblich).
Zur Konstruktion allgemeinster Typherleitungen braucht man fuer ML+ kompliziertere Beweisspezialisierungen als fuer ML, insbesondere den Umgang mit unbekannten quantifizierten Typannahmen und deren geeignete Abschwaechung.