rigide Funktionssymbole und Updates

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

rigide Funktionssymbole und Updates

Beitrag 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
Zuletzt geändert von null am 6. Feb 2013 12:48, insgesamt 1-mal geändert.

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: rigide Funktionssymbole

Beitrag von dschneid »

Konstanten werden als Funktionen mit 0 Argumenten aufgefasst. Das wurde im Foliensatz über FO-Logik so eingeführt.

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: rigide Funktionssymbole

Beitrag 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

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: rigide Funktionssymbole und Updates

Beitrag 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.

Antworten

Zurück zu „Archiv“