Seite 1 von 1

rigide Funktionssymbole und Updates

Verfasst: 6. Feb 2013 10:26
von null
Hallo zusammen,

ich wiederhole gerade den elften Foliensatz, der die dynamische Logik einführt. Dabei wird zwischen rigiden und nicht rigiden Funktionssymbolen unterschieden. Als Beispiel für rigide Funktionssymbole, also solche, die im jedem Zustand dieselbe Interpretation haben, wurde folgendes gegeben:

F = {+,-,0,1,...}

0 und 1 sind ja eigentlich Zahlen. Heißt das, dass sie hier als Funktionen angesehen werden, die den konstanten Rückgabetype 0 bzw. 1 haben?

Vielen Dank für die Hilfe
null

Re: rigide Funktionssymbole

Verfasst: 6. Feb 2013 11:13
von dschneid
Konstanten werden als Funktionen mit 0 Argumenten aufgefasst. Das wurde im Foliensatz über FO-Logik so eingeführt.

Re: rigide Funktionssymbole

Verfasst: 6. Feb 2013 12:48
von null
Ok. Daraus schließe ich, dass meine Annahme richtig ist.

Ich habe noch eine andere Frage. Im zwölften Foliensatz geht es um Updates. Im Nachhinein ist mir nicht mehr klar, wo der Unteschied zwischen einem Update und einer Zuweisung liegt. Auf Folie 9 steht folgendes:

v := t ist ein Update, wenn v eine Programmvariabel und t eine FOL - Formel ist.

Eine FOL Formel kann Quantoren beinhalten. Wie kann ich einer Variabel solch eine Formel "zuweisen". Kann mir hier jemand auf die Sprünge helfen?

Vielen Dank

Re: rigide Funktionssymbole und Updates

Verfasst: 6. Feb 2013 17:41
von Nathan Wasser
Das ist nicht ganz korrekt. "t" ist keine FOL-Formel, sondern ein FOL-Term (der auch noch typkorrekt sein muss). Dadurch sind Quantoren schon mal weg.