12 - Theorie der Programmierung (ThProg) [ID:3939]
50 von 453 angezeigt

Wir setzen fort unseren Zucht durch die Gemeinde. Genauer gesagt durch Features, die man so gängiger

massen in Programmiersprachen findet. Thema heute Induktive Datentyp. Das ist also eins der

zentralen Features, insbesondere in funktionalen Programmiersprachen. Es ist das, was die

funktionalen Programmiersprachen so rein an Ausdrucksmächtigkeit den meisten

imperativen und objektorientierten Sprachen dann doch voraus haben, sofern man nicht mit

objektorientierten Sprachen umgeht, wo also dieses Konzept der Induktiven Datentypen sehr mühsam

nachgestellt wird. Wir kennen das alle, wo man in C so eine Liste mühsam und

fehlertrechtig durch hin und her schieben mit Pointeren, gut in Java etwas harmloser mit

Referenzen nachstellen muss, ist das in Sprachen wie Heskel einfach ein flexibles und eingebautes,

natives Konstrukt der Sprache. Beispiel. Ich setze da mal tentativ nur Nummer eins vor,

dass ich die Numerierung tatsächlich durchhalte, will ich jetzt nicht versprechen. Also angenommen,

ich würde jetzt in Heskel arithmetische Funktionen programmieren wollen und würde

feststellen, es gibt da gar keine natürlichen Zahlen. Warten wir erst einmal, dass sich hier die

Aufregung gelegt hat.

Dann wäre also ein möglicher erster Versuch, sich die natürlichen Zahlen in Heskel nachzubauen.

Dieser hier, so ich weiche jetzt etwas von üblicher Heskel-Syntax ab, ist das tatsächlich

noch legales Heskel, jetzt hier einen Haufen Konstruktoren zu schreiben oder vielleicht auch nicht.

Ist auch egal. Also ich sage, welchen Datentyp ich jetzt deklariere, hinter WHERE kommt ein

Haufen Konstruktoren für den Datentyp, zum Beispiel sage ich null ist eine natürliche Zahl. Gut,

ich möchte alle Konstruktoren gerne als Funktion schreiben, deswegen schreibe ich hier die null

als Funktion mit keinem Argument, nicht so wie wir das ja generell uns von Konstanten vorgestellt hatten.

Und der andere Konstruktor ist dann die Successor-Funktion, kennen wir im Grunde schon.

Und das ist eben ein Konstruktor, der aus einer natürlichen Zahl wieder eine natürliche Zahl

konstruiert. Ja, was tue ich hier in unserer jetzt aufgebauten Sprache in diesem Moment nun?

Ich definiere schlicht und einfach eine Signatur. Ich deklariere einen Haufen Symbole und sage,

was so deren Stelligkeit ist, einmal nullstellig, einmal einstellig. Typische Buchstabe für eine

Signatur war Sigma. Sagen wir hier also der Klarheit halber, das ist die Signatur der

natürlichen Zahlen, Sigma natt. Ja, was war eine Signatur? Eine Signatur war im einfachsten Fall

so wie hier schlicht und einfach eine Menge von Funktionssymbolen gegebener Stelligkeit. Und diese

Funktionssymbole in der Signatur, die benennen wir eben, also belegen wir mit noch einem zweiten

Namen, um wieder besser auf die übliche Terminologie in Programmiersprachen zu matchen.

Wir nennen die also Konstruktoren, so wie ich das beim Erläutern des Beispiels auch schon getan habe.

So, und jetzt nach dem halben Semester reiner Syntax, kümmern wir uns mal wieder so ein bisschen

um die Semantik. Also, was meinen wir außer dieser syntaktischen Diktaturdeklaration mit dieser

Datentypdeklaration semantisch? Semantisch heißt, wir interpretieren jetzt ernsthaft

syntaktisches Material durch mathematische Objekte. Wir haben schon gesehen, so eine Pseudo-Semantik,

letztes Mal, wo wir syntaktisches Material im Grunde wieder durch syntaktisches Material

interpretieren. Hier nehmen wir echte mathematische Objekte, auch wenn es gleich erst mal nicht so

aussieht. Also, die Semantik dieser Deklaration, die drücken wir wieder durch Semantikklammern aus.

Also, ich habe jetzt hier kurz gesagt eine Semantik von Nat, natürlich in Wirklichkeit eine Semantik

dieser gesamten Deklaration, aber da schreiben wir hier die Finger, in denen ich dann immer explizit

diese ganze Deklaration dazwischen meine Semantikklammern schreibe, also mit Nat meine ich

diese Deklaration hier. Und das ist eine Mängel zunächst mal, nämlich konkret die Terme über

dieser Signatur, die ich ohne Variablen bilden kann, die geschlossenen Terme. Ja, das ist zunächst

mal natürlich doch wieder Syntax, aber wir sehen dieses Ding jetzt an als ein semantisches,

nicht mehr syntaktisches Objekt, folgender Maß. Also, erst mal erinnern wir uns, was das als Mängel

so ist. Was für Terme kann ich ohne Variablen in dieser Signatur bilden? Das haben wir schon ein

paar Mal durchexerziert, man kann zunächst mal die Null bilden. Das ist, ohne vorher Terme

konstruiert zu haben, der einzige, den ich so aus dem Stand hinschreiben kann. Naja, wenn ich den

mal konstruiert habe, dann kann ich Successor drauf anwenden. Nicht Successor von Null. Naja,

Zugänglich über

Offener Zugang

Dauer

01:17:27 Min

Aufnahmedatum

2014-05-26

Hochgeladen am

2014-05-28 12:31:42

Sprache

de-DE

Tags

Reflexiv transitiv Präordnung Äquivalenz Kontext Signatur TermErsetzungssystem
Einbetten
Wordpress FAU Plugin
iFrame
Teilen