Wozu 2 Interpreter?

Benutzeravatar
itportal2
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 236
Registriert: 25. Jan 2008 15:34
Wohnort: Darmstadt

Wozu 2 Interpreter?

Beitrag von itportal2 »

Ich kann irgendwie nicht verstehen wieso wir 2 Interpreter haben - ein symbolischer (sym-eval) und ein normaler (evalp)? Sie machen ja fast das gleiche, nur Stuck Terme werden unterschiedlich behandelt, oder?

xAx
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 157
Registriert: 6. Mär 2008 17:20

Re: Wozu 2 Interpreter?

Beitrag von xAx »

evalp kann nur call by value, also eine funktion nur mit konstruktorgrundtermen als formale parameter auswerten. das hilft einem jedoch nicht weiter, wenn man beweise von lemmata führen will, wo die variablen allquantifizert sind und somit nicht ausrechenbar sind. symbolisch kann man hier jedoch mit den diversen HPL regeln einiges erreichen.
Nichts ist wie es scheint!
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
Zuletzt geändert von xAx am 14. Mär 2009 16:17, insgesamt 99-mal geändert.

Simon Siegler
Computerversteher
Computerversteher
Beiträge: 369
Registriert: 16. Apr 2007 09:12

Re: Wozu 2 Interpreter?

Beitrag von Simon Siegler »

So ist es. evalp dient vor allem dazu, die Semantik der Sprache zu definieren. Für das führen von Gleichheitsbeweisen ist er jedoch ungeeignet, da er nicht symbolisch mit Variablen rechnen kann.

Christoph Walther
Dozentin/Dozent
Beiträge: 86
Registriert: 1. Nov 2005 18:51

Re: Wozu 2 Interpreter?

Beitrag von Christoph Walther »

Simon Siegler hat geschrieben:So ist es. evalp dient vor allem dazu, die Semantik der Sprache zu definieren. Für das führen von Gleichheitsbeweisen ist er jedoch ungeeignet, da er nicht symbolisch mit Variablen rechnen kann.
Anders gesagt: Mit evalP wird gerechnet. Z.B. "2+2" wird zu "4" ausgerechnet und "2+2=4" wird zu "true" ausgerechnet.
Der symbolische interpreter ist ein (automatischer) beweiser. Man hätte ihn also auch "Beweiser" nennen können. Der name "symbolischer interpreter" soll lediglich daran erinnern, daß sich dieser beweiser 'ähnlich' dem interpreter evalP verhält, denn er 'rechnet' auch ausdrücke aus, die symbole (also keine werte) enthalten. Z.B. wird "0+x" symbolisch zu "x" ausgewertet.

Antworten

Zurück zu „Archiv“