Matching f(x)=a

linn
Mausschubser
Mausschubser
Beiträge: 77
Registriert: 15. Okt 2008 21:16

Matching f(x)=a

Beitrag von linn »

Gibt es einen Matcher für t=f(x) und q=a?
Mit dem Kalkül kann man keine Regel anwenden, also gibt es keinen Matcher.
Aber könnte man nicht x/f^-1(a) ersetzen, falls f^-1 existieren würde?

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Matching f(x)=a

Beitrag von mister_tt »

<gewaehr_aus>
Das Kalkül ist korrekt und vollständig. Kann keine Regel mehr angewendet werden, gibt es also keinen Matcher.
</gewaehr_aus>

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

Re: Matching f(x)=a

Beitrag von Christoph Walther »

linn hat geschrieben:Gibt es einen Matcher für t=f(x) und q=a?
Mit dem Kalkül kann man keine Regel anwenden, also gibt es keinen Matcher.
Korrekt.
linn hat geschrieben: Aber könnte man nicht x/f^-1(a) ersetzen, falls f^-1 existieren würde?
Ja schon, wenn es denn so wäre. Dann würde man unter einer Gleichheitstheorie matchen. Die theorie wäre hier {all y. f(f^-1(y) = y}. Allgemein geht es also darum, wie man gleichungen in beweisen anwendet - explizit oder durch Matching. Einige Gleichungstheorien (nicht jede beliebige!) kann man in das Matching integrieren. Beispielsweise "Assoziativität". Es gilt "all x, y, z : list[@A] x <> (y <> z) = (x <> y) <> z". Damit kann man z.B. length(a <> (b <> c)) auf length((a <> b) <> c) mit der leeren substitution als lösung matchen. In VF3.2.2 ist das aber nicht implementiert, im neuen system ist "Matching unter Theorien" aber drin (=> Bachelorarbeit).

linn
Mausschubser
Mausschubser
Beiträge: 77
Registriert: 15. Okt 2008 21:16

Re: Matching f(x)=a

Beitrag von linn »

alles klar, danke

Antworten

Zurück zu „Archiv“