Formales System

Ein Formales System ist ein System von Symbolketten und Regeln, die die Umwandlung einer Symbolkette in eine andere ermöglichen. Die Anwendung der Regeln kann dabei ohne Kenntnis der Bedeutung der Symbole erfolgen.

Ein formales System kann z.B. alle Kleinbuchstaben und das Leerzeichen als Symbole haben. Symbolketten können beliebige Folgen von – sinnvollen und sinnlosen – Wörtern sein (es geht nur um die Symbole, also Buchstaben). Eine mögliche Symbolkette ist hier:

er kam sah siegte

Als einzige Regel ersetzt man jeden Buchstaben durch seinen Nachfolger im Alphabet, also a durch b, b durch c und so fort. z wird durch a ersetzt. Aus der obenstehenden Symbolkette wird durch Anwendung der Regel:

fs lbn tbi tjfhuf

Dieses System wurde zur Verschlüsselung von Nachrichten eingesetzt, wie es schon in ähnlicher Form von Julius Cäsar verwendet wurde. Zur Entschlüsselung benutzt man ein gleichwertiges formales System, das jeden Buchstaben durch seinen Vorgänger ersetzt:

er kam sah siegte

Man kann die Regel auch mehrfach anwenden. Bei zweifacher Anwendung erhält man

gt mco ucj ukgivg

Logik

Formale Systeme werden in der Logik zur exakten Untersuchung der Bedingungen für das Folgern einer Aussage eingesetzt.

Ein berühmtes Beispiel für ein formales System ist das MU Rätsel aus dem Buch Gödel, Escher, Bach:

Das formale M,I,U-System

Das System besteht aus drei Symbolen‚ M, I und U. Symbolketten können durch die folgenden vier Regeln in andere Ketten verwandelt werden:

Regel1: Wenn das letzte Symbol I ist, kann U angefügt werden (aus MI wird MIU)

Regel2: Aus Mx kann Mxx erzeugt werden (aus MIU wird MIUIU)

Regel3: III kann durch U ersetzt werden (aus MUIIII wird MUIU)

Regel4: UU kann gestrichen werden (aus MUUUI wird MUI)

Das MU-Rätsel

1. Vorgegeben ist die Symbolkette MI
2. Gibt es eine beliebige Folge der Anwendung der Regeln, so dass die Symbolkette MU aus MI entsteht?

Die Aufgabe kann nicht durch einfaches Erzeugen aller möglichen Symbolketten (Brute Force-Suche) gelöst werden.

Mathematik

In der Mathematik bestehen formale Systeme aus Axiomen und Schlussfolgerungs-Regeln. Mathematische Sätze lassen sich aus den Axiomen und bereits bewiesenen Sätzen durch Anwendung der (Rechen-)Regeln gewinndne. Die Beweisbarkeit eines mathematischen Satzes ergibt sich aus der Möglichkeit der Erzeugung des Satzes aus den Axiomen mit Hilfe der Regeln.

Ein klassisches Beispiel für ein axiomatisches System ist die Gruppentheorie. Eine Gruppe lässt sich über einer Menge und einer zugehörigen (Rechen-)Operation bilden. Mathematische Sätze lassen sich allein aus den vier Axiomen der Gruppe gewinnen. Die Sätze gelten dann für alle Mengen mit zugehöriger Operation, deren Eigenschaften sich auf die Gruppenaxiome abbilden lassen.

Informatik

In der theoretischen Informatik dienen formale Systeme zur exakten Wiedergabe der inneren Logik eines Systems. Formale Sprachen, die aus einem Alphabet von Symbolen und zughörigen Worten als Symbolketten bestehen, sind ein Hilfsmittel hierzu. Die Syntax wird durch eine zugehörige Grammatik festgelegt, über die die Gültigkeit der Worte festgestellt werden kann. Die Semantik des formalen Systems ist damit aber noch nicht eindeutig definiert.

Definition der Syntax von Programmiersprachen

Ein Untersuchungsgegenstand hierzu ist die Möglichkeit einer Definition von realen Programmiersprachen über ein formales System. Als Beispiel mag hier der Aufruf von Unterprogrammen mit Parametern dienen. Die Syntax für die Unterprogrammdefinition und den Programmaufruf kann über eine formale Sprache und die zugehörige formale Grammatik definiert werden.

In der Sprache Pascal kann beispielsweise ein Unterprogramm über

PROCEDURE example(A, B: integer; VAR C: result); BEGIN .. END;

definiert und später dann über

example(2*X,Y,W);

aufgerufen werden.

Ein möglicher Ausschnitt der formalen Grammatik zur Syntaxdefinition in erweiterter Backus Naur Notation könnte dann sein:

procedure_declaration = PROCEDURE name 
                          '(' formal_parameter_list ')' block ';'
block = BEGIN ... END
formal_parameter_list = parameter { ';' parameter } ;
parameter = [ VAR ] name ':' name ;

...
procedure_call = identifier '(' actual_parameter_list ')' ';' ;
actual_parameter_list = expression { ',' expression } ;

Symbole sind hier procedure_declaration, identifier, formal_parameter_list, aber auch '(', ':', VAR usw. Eine Symbolkette auf der rechten Seite des Gleichheitszeichens wird, falls sie auftritt, durch das Symbol auf der linken Seite ersetzt. Die Symbolkette und damit das ersetzte Symbol kann wiederum Teil einer Symbolkette sein.

Ein gegebener Programmtext ist syntaxfehlerfrei, wenn er durch die Umwandlungsregeln der formalen Grammatik auf ein einzelnes Symbol, z.B. program, reduziert werden kann.

Hätte man eine Sprache, die definiert wird durch

program = PROGRAM { procedure_declaration } BEGIN 
               BEGIN { procedure_call } END '.'

so bestünde ein konkretes Programm nur aus Unterprogramm-Deklarationen und Aufrufen: Das reale Programm

PROGRAM 
   PROCEDURE p1(a: integer; b: integer)
     BEGIN ... END;
   PROCDURE p2(VAR x: integer)
     BEGIN ... END;
BEGIN 
    p1(0,1);
    p2(y);
END.

könnte man mit obenstehendem (unvollständigen) Grammatikausschnitt reduzieren:

Schritt1:

PROGRAM 
   PROCEDURE name(name: name; name: name)
     block;
   PROCEDURE name(VAR name: name)
     block;
BEGIN 
    name(expression,expression);
    name(expression);
END.

Schritt2:

PROGRAM 
   PROCEDURE name(formal_parameter_list)
     block;
   PROCEDURE name(formal_parameter_list)
     block;
BEGIN 
    name(actual_parameter_list);
    name(actual_parameter_list);
END.

Schritt3:

PROGRAM 
   procedure_declaration
   procedure_declaration
BEGIN 
    procedure_call;
    procedure_call;
END.

Schritt4:

program 

Das Programm ist damit syntaktisch korrekt. Es ist aber nicht die ganze Logik des Programms überprüft worden:

• Die Übereinstimmung der Namen wurde nicht überprüft (man hätte auch p3 statt p2 aufrufen können).
• Die Art der Parameterübergabe ist nicht definiert.
• Typüberprüfung findet nicht statt.
• ...

Diese Eigenschaften werden unter dem Begriff Semantik im Gegensatz zur Syntax zusammengefasst.

Linguistik

In der Linguistik werden formale Systeme zur Definition von formalen Sprachen verwendet, deren Symbolbedeutung undefiniert ist und deren Anwendung allein aufgrund der Regeln erfolgt.

Literatur

Dougles. R. Hofstaedter: Gödel, Escher, Bach, ein endlos geflochtenes Band, DTV, ISBN 3423300175

Weblinks

Lösung des MU Rätsels