Praktikum 3 - MATCH-Funktion

[mister_tt]

Hallo zusammen,

Meine Gruppe und ich stehen gerade auf dem Schlauch... Warum führt der Aufruf MATCH(var(variable(0)) :: apply(func(0), ø) :: ø, var(variable(0)) :: apply(func(0), ø) :: ø) zu einem Blitz!? In unserer Kalkül-Darstellung wäre das doch \(\lbrace \lbrace v_0 \doteq v_0 ; f_0() \doteq f_0() \rbrace , \lbrace \rbrace \rbrace\) und das können wir doch mit Eliminate und anschließendem Decompose (was mit leerer Parameterliste doch ebenfalls ein Eliminate ist) auflösen...

Viele Grüße,
Simon, Christian, Nadine und Ini

[pigbird]

Hallo, ich habe die MATCH-Funktion nicht im Kopf, aber ich glaube die MATCH Funktion liefert uns eine Substitution (Result) nur wenn die zweite Liste saemtlich Grundterme enthaelt, was in deinem Beispiel nicht der Fall ist, und fuehrt zu einem Blitz.

[_Peter_]

hmmm, das gleiche wollt ich auch grad fragen, sogar extra ne schöne Grafik erstellt gehabt:



Edit: Ach, da warn Fehler drin, man merkt, dass ich schon zu lang dran sitze, 5,6 und 7 müssten apply(func(), ø) sein.
Dann spuckt er Matcher aus...

[Manolis]

Selbes Problem, keine Lösung. Die einzige Eingabe, die keinen ↯ ausgibt ist MATCH(ø, ø). Da kommt - wie zu erwarten war - return(ø) raus...
Hat noch jemand eine gültige Eingabe gefunden? Oder muss man bei den Eingaben etwas beachten?

edit: Ok, hat sich geklärt! Ganz dummer Fehler!!!

[pigbird]

wie gesagt, die zweite Liste, die MATCH-Funktion bekommt, darf nur Grundterme enthalten. Das Beispiel von mister_tt wird mit einer kleinen Änderung funktionieren:

Code: Alles auswählen

MATCH(var(variable(0)) :: apply(func(0), ø) :: ø, apply(func(0), ø) :: apply(func(0), ø) :: ø)

[Manolis]

JA, zu beachten ist bei dem Problem Folie 31 aus Foliensatz 4. Das hab ich auch zuerst übersehen.

Das Matchingproblem
• Gegeben:
– Term t ∈ T (Σ, V) (genannt Pattern) sowie
– Grundterm q ∈ T (Σ) (genannt Target)

Auszug aus Beispiel 1:

Für t = h(g(x), y) und q = h(g(f (a)), h(a, f (b)))
(mit x, y ∈ V und f, g, h, a, b ∈ Σ)...

alle "Variablen" aus dem Target sind also aus Σ!

Hoffe, das hilft weiter

und @ _Peter_:

Code: Alles auswählen

MATCH(
apply(func(4), apply(func(3), var(variable(0)) :: ø) :: var(variable(1)) :: ø) ,
apply(func(4), apply(func(3), apply(func(2), apply(func(0), ø) :: ø) :: ø) ::
      apply(func(4), apply(func(0), ø) :: apply(func(2), apply(func(1), ø) :: ø) :: ø) :: ø))

das sollte dein Problem lösen