Beziehung zwischen formalem System und formalen Sprachen

In einem Informatikkurs ist es üblich, die Hierarchie formaler Sprachen, Grammatiken, Automaten und Turing-Maschinen zu studieren. Ich frage mich, in welcher Beziehung diese Objekte zu formalen Systemen stehen.

Zum Beispiel soll Lambda-Kalkül ein formales System sein. Würde seine Grammatik auch als formales System betrachtet werden?

Meiner Meinung nach sollte ein formales System haben

1. Eine gut definierte Reihe von Symbolen .
2. Eine gut definierte Grammatik , die zeigt, wie wohlgeformte Formeln aus den Symbolen aufgebaut sind.
3. Ein oder mehrere gut definierte Inferenzkalküle , die ähnlich wie der mit einer Grammatik verbundene Inferenzkalkül funktionieren könnten.
4. Eine oder mehrere Semantiken , die es ermöglichen, den Formeln, Sätzen und Aussagen des formalen Systems eine Bedeutung zuzuweisen.

Auch wenn der letzte Punkt angefochten werden könnte, ist er derjenige, der für den signifikanten Unterschied zwischen einem formalen System und einer Grammatik oder einer formalen Sprache verantwortlich ist. Der Inferenzkalkül eines formalen Systems könnte tatsächlich mit dem Kalkül einer Grammatik übereinstimmen, obwohl er normalerweise nicht mit dem Kalkül der Grammatik des formalen Systems selbst übereinstimmt.

(Sogar eine Grammatik kann mehrere Inferenzkalküle haben, aber die Verwendung mehrerer Inferenzkalküle für ein formales System ist in der Logik üblicher, wenn Sie Dinge wie die Eliminierung von Schnitten beweisen oder ein formales System als Grundlage für eine Hierarchie formaler Systeme verwenden möchten .)

Eine formale Sprache ist sowohl einer Grammatik als auch einem formalen System zugeordnet. Für ein formales System sind sowohl die Menge wohlgeformter Formeln als auch die Menge gültiger wohlgeformter Formeln formale Sprachen. Die formale Sprache ist eine Art Äquivalenz, die sich aus dem Ignorieren zusätzlicher Strukturen wie der Semantik des Inferenzkalküls oder der feineren Teile einer Grammatik ergibt. Es ist eine offensichtliche Verbindung zwischen formalen Systemen und Grammatiken, aber formale Systeme und Grammatiken können enger verwandt sein als durch eine formale Sprache allein ausgedrückt werden (dh sie können einen äquivalenten Inferenzkalkül haben).

Im Allgemeinen besteht ein formales System aus

• eine Sprache, die ihre wohlgeformten Formeln von den nicht wohlgeformten Zeichenketten unterscheidet
• eine Art Semantik , die besagt, welche Formeln wahr sind und welche nicht
• Axiome und Inferenzregeln, die versuchen, rechnerisch genau die Formeln zu erzeugen, die angesichts der Semantik wahr sind.

Wir können die Sprache wohlgeformter Formeln mithilfe einer Grammatik spezifizieren, aber eine Grammatik ist selbst kein formales System.

Eine formale Sprache $\mathcal{L}$ besteht aus:

• ein Alphabet von Symbolen, dh eine Reihe von Symbolen mit der Besonderheit, dass jedes dieser Symbole ohne Bezugnahme auf eine Interpretation angegeben werden kann. Das Alphabet einer formalen Sprache$\mathcal{L}$ wird oft als bezeichnet $\Sigma$.

• Eine Grammatik , die bestimmt, in welchen Folgen von Symbolen$\Sigma$sind gut definierte Formeln (oft als wffs bezeichnet ) in$\mathcal{L}$.

Ein formales System $\mathcal{S}$ ist:

• Eine formale Sprache $\mathcal{L}$
• Ein deduktiver Apparat.

Was ist ein deduktiver Apparat, den Sie fragen können?

• Eine beliebige Menge von wffs in$\mathcal{L}$das sind Axiome

• Eine Reihe von Inferenzregeln , die bestimmen, welche wffs eine Beziehung von "unmittelbarer Konsequenz" zwischen ihnen haben.

Hier sind einige ausgezeichnete Referenzen, ob Sie anfangen oder in fleischigere Sachen eintauchen möchten:

• Metalogic: Eine Einführung in die Metatheorie der Standardlogik erster Ordnung von Geoffrey Hunter.

• Automaten, formale Sprachen und algebraische Systeme von Masami Ito

Was Sie in einem Einführungskurs in formale Sprachen sehen, ist nur eine kleine Auswahl der Vielzahl von Modellen, die zum formalen Definieren und Studieren von Sprachen (oder Funktionen, Zahlen usw.) verwendet werden, dh hinsichtlich ihrer syntaktischen Struktur - die eine dynamische Komponente hat. was wir "Berechnung" nennen - abgesehen davon, was als ihr Inhalt angesehen werden könnte , um a posteriori oder überhaupt nicht wieder an diese Strukturen gebunden zu werden . Diese unterschiedlichen Modelle stammen aus unterschiedlichen Kontexten und haben unterschiedliche theoretische und praktische Anwendungen.

Die zur Beschreibung dieser Modelle verwendete Sprache kann auch formalisiert werden, sodass Sie Grammatiken sowohl als formale Systeme als auch als Sprachen verwenden können. Diese Art von Zirkularität ist problematisch, aber unvermeidlich und in vielen Fällen wünschenswert.

Der Begriff des formalen Systems, wie er in der Informatik verwendet wird, hat historisch mit der Untersuchung formaler Eigenschaften mathematischer Logiksysteme zu tun. Die Standarddefinitionen, die Sie in anderen Antworten sehen, stammen von diesem gemeinsamen Ursprung. Es gibt andere Arten von formalen Systemen in anderen Forschungsbereichen, der Begriff ist polysemisch. Die Unterscheidung zwischen Form- und Inhaltskonzepten hängt davon ab, woher Sie kommen.

Ich suche die gleiche Frage und es scheint, dass es keine Klarheit gibt. Ich hoffe jemand konnte uns geben.

Siehe zum Beispiel, was Levelt in seinem Buch (" Eine Einführung in die Theorie formaler Sprachen und Automaten ", Kap. 1, S. 1) gesagt hat:

Aus mathematischer Sicht sind Grammatiken FORMALE SYSTEME wie Turing-Maschinen, Computerprogramme, Präpositionallogik, Inferenztheorien, neuronale Netze usw. [ 1 ]

Trotzdem ist es wirklich wichtig, auf welche anderen Antworten hier hingewiesen wird, da formale Grammatiken einige grundlegende Attribute (dh deduktive Apparate), die als formale Systeme gekennzeichnet sind, wirklich zu übersehen scheinen.

Wenn eine Turing-Maschine jedoch ein formales System ist [ 2 ] und formale Sprachen (und ihre Darstellungen, Grammatiken) diesen entsprechen: Warum ist Grammatik auch kein formales System?

Ich hoffe, dass diese Überlegung, obwohl das Ereignis nicht schlüssig ist, eine verbesserte Antwort auf dieses Problem hervorrufen kann.