Ocaml: Aussagenlogik < Formale Sprachen < Theoretische Inform. < Hochschule < Informatik < Vorhilfe
|
| Aufgabe | Schreiben sie zu dieser Signatur in Ocaml den dazugehörigen Befehl:
(* liefert die Liste der Aussagen in der alf )*
val aussagen : alf −> char list |
type alf =
| Konst of bool (* Wahrheitswerte *)
| Var of char (* atomare Formel *)
| Nicht of alf (* Negation *)
| Und of alf * alf (* Konjunktion *)
| Oder of alf * alf (* Disjunktion *)
| Aequi of alf * alf (* Aequivalenz *)
| Biaequi of alf * alf (* Biaequivalenz *)
;;
type belegung = true | false
;;
Diese Befehle hab ich in Ocamlschon programmiert und sie sollten passen. Wie kann ich jetzt aber dazu die gesuchte Funktion schreiben?
Sie sollte mir alle Aussagen aus dem typ alf liefern, aber ich kommnicht dahinter wie ich das lösen soll!
Danke für eure Hilfe!!
Michael
|
|
| |
|
Hallo,
> Diese Befehle hab ich in Ocamlschon programmiert und sie sollten passen.
Korrekter: Du hast gerade die Datentypen "alf" und "belegt" definiert.
> Sie sollte mir alle Aussagen aus dem typ alf liefern, aber ich kommnicht dahinter wie ich das lösen soll!
Schwierig... Es gibt unendlich viele Aussagen, weil der Datentyp rekurisv definiert ist. Also musst du noch Zusatzwissen haben. Wie kommst du auf diesen Datentyp? In welchem Zusammenhang steht diese Aufgabe?
Gruß
Martin
|
|
|
| |
|
das aufgabenblatt befindet sicher hier:
++
Ausgegeben sollten nur die Aussagen also die Variablen in den einzellnen Gesamtaussagen. Mein problem ist es dass ich es nicht schaffe auf sie alle einzelln zu zu greifen.
+++
|
|
|
| |
|
Hallo,
schau dir mal genauer an, was mit Belegungen gemeint ist. Deine Lösung ist auf jeden Fall falsch!
Deine Funktion aussagen ist nicht rekursiv, weil sie sich niemals selbst aufruft. Somit kannst du nicht beliebig verzweigte Ausdrücke verarbeiten.
Außerdem musst du alle Konstruktoren abdecken.
Beim Auftreten eines Konst-Konstruktors gibst du einfach eine leere Liste zurück.
Beim Auftreten eines Var-Konstruktors gibst du eine einelementige Liste zurück, die das dazugehörige char enthält.
Beim Auftreten eines Nicht-Konstruktors rufst du die Funktion rekursiv auf dem Argument auf.
Beim Auftreten der übrigen Konstruktoren (je zwei Argumente) rufst du die Funktion zweimal rekursiv auf den beiden Argumenten auf und verbindest die Ergebnislisten mit dem @-Operator.
Fertig!
Außerdem: Es heißt Implikation und Äquivalenz, nicht Äquivalenz und Biäquivalenz!!!
Gruß
Martin
|
|
|
| |
|
also ich bin dann soweit:
type alf =
| Konst of bool (* Wahrheitswerte *)
| Var of char (* atomare Formel *)
| Nicht of alf (* Negation *)
| Und of alf * alf (* Konjunktion *)
| Oder of alf * alf (* Disjunktion *)
| Impl of alf * alf (* Aequivalenz *)
| Aequi of alf * alf (* Biaequivalenz *)
;;
type belegung ++
+++
bis hierher funktioniiert alles soweit!
ich habde dann für die funktion variablen das ganze so programmiert:
++
die auch funktionieren sollte
dann die funktion:
let passt a b = aussagen a = variablen b;;
und dann für die funktion aussagen diese funktion, die eigentlich funktionieren sollte nur bin ich mir nicht ganz sicher ob es so passt und wie ich es für Impl und Aequi machen soll!
+++
( liefert eine schön formatierte Zeichenkette für alf )
++
Es wäre super, wenn sich jemand das alles anschauen würde und mir eventuell wieder weiterhelfen würde!!!!
lg Michael
|
|
|
| |
|
Hallo,
das sieht ja schon recht ordentlich aus!
> bis hierher funktioniiert alles soweit!
Ja, muss es!
> ich habde dann für die funktion variablen das ganze so programmiert:
> let rec variable (b:belegung) = match b with
> | (hr, hk)::t -> hr::(variable t)
> | [] -> [];;
> die auch funktionieren sollte
Hast du die nicht ausprobiert? Solltest du mal. Sieht aber richtig aus.
> dann die funktion:
> let passt a b = aussagen a = variablen b;;
Du meintest eher "aussagen a == variablen b".
Ein 1:1-Vergleich ist aber zu einfach. aussagen kann dir nämlich ein Liste liefern wie ['y'; 'y'; 'x']. Wenn du das mit deiner Variablenliste ['x'; 'y'] vergleichst, bekommt du ein false als Antwort, obwohl alles passt.
Du soltest einfach für jedes Element der ersten Liste prüfen, ob es in der zweiten Liste vorkommt. Also: Rekursion über beide Listen!
> und dann für die funktion aussagen diese funktion, die eigentlich funktionieren sollte nur bin ich mir nicht ganz sicher ob es so passt und wie ich es für Impl und Aequi machen soll!
Falscher Funktionsname, aber macht nichts.
In lookup hast du schon wieder = statt == bei einem Vegleich geschrieben. Immer schön testen!
Eine Implikation [mm] $A\Rightarrow{}B$ [/mm] lässt sich auch schreiben als [mm] $\neg{A}\vee{}B$
[/mm]
Eine Äquivalenz [mm] $A\Leftrightarrow{}B$ [/mm] kannst du im Programm mit == erreichen (oder mit Implikationen in beiden Richtungen).
> Und zu der letzten Signatur fällt mir leider überhaupt nichts ein:
Wieso nicht? Wieder rekursiv vorgehen:
Basisfälle Konst und Var, da kannst du entweder die Konstanten "0" und "1" zurückgeben oder die Namen der Variablen (hier verweise ich auf die Funktion String.make).
Alles andere ist rekursiv: Du gibst das Zeichen für diese logische Verknüpfung aus und rufst deine Funktion rekursiv auf dem Rest auf. Wichtig ist hier, dass die Operatoren infix notiert werden, also, dass sie in der Mitte stehen. Die beiden Aufrufe stehen also jeweils links und rechts vom Operator-String. Eine Verkettung von Strings erreichst du per ^. Um die Klammern kannst du dich kümmern, wenn der Rest steht.
Versuch es. Programmier zuerst die Basisfälle (und vielleicht das Nicht) und teste die Funktion! Es gibt zwar eine Warnung, weil nicht alle Fälle abgedeckt sind, aber wir wollen ja bloß die Syntax checken.
Frohes Schaffen!
Gruß
Martin
|
|
|
| |
|
+++
So hab ich jetzt dasletzte programmiert. Mein Problem ist jetzt wie das gemeint ist mit dem wohlgeformten. bei mir kommt halt jetzt eine signatur heraus, die so ausschaut:
- : string = " ¬ a ^ b <-> c <-> d"
ich weiß jetzt nicht ganz genau was man da genau sehen sollte! Und mein Hauptproblem ist dass ich nicht dieklammern reinbekomme weil dann fängt ocaml immer jammern an!
lg michael
|
|
|
| |
|
Hallo,
ist doch schon mal nicht schlecht, aaaaber:
Die Konstanten gehören bekanntlich auch zu den alfs, also müssen sie auch in dieser Funktion vertreten sein.
Und: Wie versprochen fehlen jetzt noch die Klammern. Da gibt es zwei Möglichkeiten:
1. Jeder Teilausdruck setzt sich selbst in Klammern oder
2. jeder Teilausdruck setzt seine Operanden, also die nächste Rekursionsstufe in Klammern.
Bei 1. hast du als Endergebnis den gesamten Ausdruck auf der obersten Ebene auch geklammert. Bei 2. sind jede Konstante und jede Variable geklammert. Mir persönlich gefällt Ersteres besser.
Und so könnte es aussehen:
# let a=Und(Oder(Konst true, Aequ(Impl(Var 'a', Nicht (Var 'b')),Var 'x')), Impl(Nicht(Oder(Konst false, Aequ(Var 'z', Konst true))), Und(Var 'a', Var 'y')));;
val a : alf = Und (Oder (Konst true, Aequ (Impl (Var 'a', Nicht (Var 'b')), Var 'x')), Impl (Nicht (Oder (Konst false, Aequ (Var 'z', Konst true))), Und (Var 'a', Var 'y')))
# string_of_alf a;;
- : string = "((1 v ((a => !b) <=> x)) ^ (!(0 v (z <=> 1)) => (a ^ y)))"
Das absolute Meisterstück wäre natürlich, wenn die Klammern nur dort gesetzt würden, wo sie benötigt werden. Da müsstest du aber jedesmal die Prioritäten der Operationen beachten...
Gruß
Martin
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 01:40 Fr 09.11.2007 | | Autor: | Martin243 |
Nur eine kleine Ergänzung. Mit Berücksichtigung der Prioritäten könnte es so aussehen:
# pri_string_of_alf a;;
- : string = "(1 v (a => !b <=> x)) ^ (!(0 v (z <=> 1)) => a ^ y)"
Gruß
Martin
|
|
|
| |
|
danke, also ich hab das jetzt mit den klammern recht schön gelöst:
- : string = "(((0 ^ b)->c)<->d)"
sollte für mein niveau reichen.
ich habe mir jetzt überlegt, dass ich die funktion passt lassen kann wie ich sie hatte, nur muss ich die ganzen variablen aus aussagen streichen, die doppelt vorkommen.
mein problem ist nur dass ich es nur schaffe die variablen zu löschen die dirket neben einander stehen zB bei Und(Var'x', Var'x') aber nicht wenn sie weiter auseinander stehen.
gibt es da eine möglichkeit das zu ändern??
ich bräuchte eine funktion die einfach doppelte listen elemente löscht zB.
danke dass du auch zu so später stunde noch zeit für mich hattest!!
lg Michael
|
|
|
| |
|
Hallo,
> ich habe mir jetzt überlegt, dass ich die funktion passt lassen kann wie ich sie hatte, nur muss ich die ganzen variablen aus aussagen streichen, die doppelt vorkommen.
OK, wenn du das getan hast, dann bleiben immer noch zwei Probleme:
1. Die Reihenfolge: Die Variablenbezeichnungen können in dem alf und in der Belegung in unterschiedlicher Reihenfolge vorkommen.
2. Zusätzliche Variablen: Eine Belegung kann beliebige Variablen enthalten. Das heißt, es können darin Variablen vorkommen, die mit deinem alf-Ausdruck nichts zu tun haben. Ein Vergleich würde scheitern. Du müsstest hier also prüfen, ob die Variablen in deinem Ausdruck eine Teilmenge der Variablen in deiner Belegung sind.
Bevor wir zu einem Lösungsansatz kommen, schauen wir erstmal weiter:
> mein problem ist nur dass ich es nur schaffe die variablen zu löschen die dirket neben einander stehen zB bei Und(Var'x', Var'x') aber nicht wenn sie weiter auseinander stehen.
> gibt es da eine möglichkeit das zu ändern??
Klar. Sortier doch einfach die Liste, bevor du die Duplikate entfernst.
Wenn du dann die andere Liste (der Variablen aus der Belegung) auch sortierst, dann hat sich auch Problem 1 gelöst.
Bleibt Problem 2: Du musst prüfen, ob die sortierte, duplikatfreie Liste A eine Teilmenge der sortierten, duplikatfreien Liste B ist.
Am besten machst du eine Rekursion über Liste A und läufst dann für jedes Element solange durch Liste B, bis du das Element findest (gut) oder das Ende erreichst (schlecht).
Es gibt bestimmt eine fertige Sortierfunktion für Listen. Vielleicht kannst du die ja benutzen...
Gruß
Martin
|
|
|
|
