Seite 1 von 1

Axiome aus Datentypdefinitionen, ?cons_i

Verfasst: 20. Feb 2012 18:37
von kbraden
Hallo,

in Kapitel 9, Abschnitt 1 Definition 1 Axiom 5 steht:
\(\forall i \in \{1,\ldots,k\}: \forall x : struct[@T_1, . . . ,@T_n]: \quad
?cons_i(x) \equiv eq_{struct}[@T_1,...,@T_n](x,cons_i(sel_{i,1}(x), . . . , sel{i,n_i}(x)))\)


Angenommen wir haben natuerliche Zahlen und wollen "?succ(0)" betrachten, so wird das ersetzt durch \(eq_{nat}(0, succ(pred(0)))\).
Da pred(0) nicht definiert ist, frage ich mich wo jetzt das "false" herkommt, was ja am Ende "rauskommen" muss. Wird ignoriert dass der Konstruktor succ einen Stuck-Term uebergeben bekommt, sodass einfach \(eq_{nat}(0, succ(\ldots)) \equiv false\) (Axiom 3) angewendet wird?

LG

Re: Axiome aus Datentypdefinitionen, ?cons_i

Verfasst: 20. Feb 2012 20:39
von Christoph Walther
kbraden hat geschrieben: Wird ignoriert dass der Konstruktor succ einen Stuck-Term uebergeben bekommt, sodass einfach \(eq_{nat}(0, succ(\ldots)) \equiv false\) (Axiom 3) angewendet wird?
Ja, genau so ist es. Denn für jeden nat-term t über der signatur eines (terminierenden!) L-programms gilt eq(0, succ(t)) = false mit axiom 3.

Re: Axiome aus Datentypdefinitionen, ?cons_i

Verfasst: 20. Feb 2012 21:40
von kbraden
Perfekt, danke.