first class functions?

DanielSchoepe
Mausschubser
Mausschubser
Beiträge: 49
Registriert: 28. Sep 2009 11:39

first class functions?

Beitrag von DanielSchoepe »

Da \(\mathcal{L}\) eine funktionale Sprache sein soll, sollte es ja möglich sein, Funktionen zu definieren die Funktionen als Argumente erhalten oder zurückgeben. Allerdings habe ich noch nicht herausfinden können wie dies zu bewerkstelligen ist. Die üblichen Notationen für Funktionstypen in den Argumenten scheinen nicht zu funktionieren. Z.B.:

Code: Alles auswählen

function test(f : nat -> nat, n : nat) <= f(n)
function test(f : nat => nat, n : nat) <= f(n)
Diese Definitionen werfen beide Syntax-Fehler da \(\mathbb{N} \rightarrow \mathbb{N}\) nicht als gültiger Typ erkannt wird. Auch in der Sprachdokumentation habe ich nichts dazu gefunden.

Sind Funktionen als Argumente nun zulässig? Wenn dies nicht möglich ist, halte ich es für etwas irreführend \(\mathcal{L}\) als funktionale Sprache zu bewerben, da dies doch ein sehr grundlegendes Feature funktionaler Sprachen ist.

Benutzeravatar
AlexPi11
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 154
Registriert: 18. Apr 2009 15:32

Re: first class functions?

Beitrag von AlexPi11 »

Ein Absatz aus dem Preface aus The L 1.0 Primer mit dem interessanten Teil hervorgehoben:
But there is another point: Since our concern is verification, it does not help to use a “real”
language containing features the verifier does not support. This would rather mean to define
subsets of the “real” language by restricting it to language features the verifier can cope with.
But it takes time to set up a verifier to support all these beautiful language features coming
with “real” functional languages. So this answers another question sometimes heard: “Why
does your language not support mutual recursion, higher-order functions, a more flexible type
system, etc.?” This is simply because we first have to develop the reasoning mechanisms for a
feature before we can integrate it into the language. And the development of those mechanisms
requires numerous experiments and tests, unfortunately always taking much more time than
expected.
Also wird sowas wohl nicht unterstützt.

Christoph Walther
Dozentin/Dozent
Beiträge: 86
Registriert: 1. Nov 2005 18:51

Re: first class functions?

Beitrag von Christoph Walther »

Mit "funktionale Programmiersprache" ist gemeint, daß "mit Funktionen" programmiert wird: Ausgehend von gegebenen grundfunktionen werden mittels funktionalkomposition und rekursion funktionen definiert, die die erwünschten berechnungen modellieren. Man verwendet den begriff "funktional" dabei als abgrenzung zu anderen programmierparadigmen, wie etwa der imperativen programmierung, der logischen programmierung, usw.

Kennzeichnend für die imperative programmierung sind die verwendung von zuweisungen und schleifenbefehlen, die in (rein) funktionalen sprachen (wie z.B. Pure LISP, L) nicht zur verfügung stehen.

Dagegen ist mit "funktional" nicht gemeint, daß prozeduren als parameter von prozeduren erlaubt sind. Schon in den ersten "klassischen" imperativen programmiersprachen wie ALGOL60 und PASCAL sind prozeduren als parameter von prozeduren erlaubt, trotzdem sind dies keine funktionalen sprachen.

Kurzum, eine funktionale programmiersprache muß nicht notwendigerweise prozeduren als prozedurparameter erlauben. Will man dies gesonders kennzeichnen, so spricht man von der "stufe" oder "ordnung" der sprache: Eine sprache der 1. stufe erlaubt nur datenobjekte als prozedurparameter, eine sprache der 2. stufe zusätzlich prozeduren der ersten stufe als prozedurparameter, usw.

In diesem sinne ist L eine funktionale sprache 1. stufe. Warum? Die antwort steht in dem zitat aus dem 2. posting. L ist schnell zu einer sprache 2. stufe erweitert, das ist nicht schwierig. Nur was ist damit gewonnen, wenn dann mit prozeduren als prozedurparameter programmiert werden kann, solche programme jedoch mangels beweisunterstützung nicht verifiziert werden können (denn um verifizierte programme geht es ja in diesem kontext)?

Um solche programme zu verifizieren sind die dazu erforderliche logik und darauf aufbauend geeignete beweismechanismen zu entwickeln. Konkret: Welche induktionsschemata sind erforderlich, um die korrektheitsbeweise zu führen, wie können solche schemata automatisch bereitgestellt werden, wie werden automatisch terminierungsbeweise für prozeduren mit prozedurparametern geführt, und so weiter und so fort. Hat man diese fragen beantwortet, dann müssen die ergebnisse softwaretechnisch in ein system umgesetzt werden. Und ist dies erledigt, dann muß das ganze schließlich in das bereits vorhandenen system integriert werden.

Der aktuelle stand: L ist zu einer sprache 2. stufe erweitert worden, die dazu entwickelten und implementierten beweistechniken haben sich in zahlreichen fallstudien bewährt, man kann also funktionale programme 2. stufe schreiben und mit VeriFun verifizieren. Der letzte schritt - die systemintegration - ist eine harte, softwaretechnische nuß, die gegenwärtig in arbeit ist.

PS: Für solche arbeiten wird die unterstützung durch studentische hilfskräfte gerne angenommen.

Antworten

Zurück zu „Archiv“