| |
| Autor |
 Beweis Symmetrie alpha-Konversion Lambda-Kalkül |
|
DerTSH
Junior 
Dabei seit: 09.12.2022
Mitteilungen: 14
 |  Themenstart: 2023-04-01
|
Hallo zusammen, ich gehe gerade https://www21.in.tum.de/teaching/logik/SS13/lambda.pdf durch und wollte Lemma 1.1.7 auf Seite 7 beweisen. Hier geht es um die Aussage, daß die alpha-Äquivalenz symmetrisch ist.
Ich habe:
C = Context; s, t, u = Term; x, y = Variablen. Definition der alpha-Konversion wie im Script.
Mein Ansatz:
https://matheplanet.com/matheplanet/nuke/html/uploads/c/56027_Screenshot_2023-04-01_185528.png
Ich versuche über FV(x.u) an FV(u) OHNE x zu kommen, um damit die Substitution für die andere Richtung hinzubekommen, bin mir aber nicht sicher, ob das so paßt. Ich wäre dankbar, wenn da mal wer drüberschauen könnte.
|
 Profil
|
tactac
Senior 
Dabei seit: 15.10.2014
Mitteilungen: 2796
 | Beitrag No.1, eingetragen 2023-04-01
|
\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]}
\newcommand{\name}[1]{\ulcorner#1\urcorner}
\newcommand{\upamp}{\mathbin {⅋}}
\newcommand{\monus}{\mathbin {∸}}\)
$u[y/x]$ ist nicht $u$. Jedenfalls nicht allgemein unter den weiteren geltenden Dingen. $u[y/x]=u$ könnte man schließen, wenn man wüsste, dass $x \notin FV(u)$. Du hast aber nur $y \notin FV(u)$.
Des weiteren sind die Daten, die du als geltend angibst, solche für $s \to_\alpha t$. $s =_\alpha t$ ist aber 'was anderes.
Es kann aber sein, dass man $s \to_\alpha t \implies t \to_\alpha s$ tatsächlich zeigen kann. Um das präzise zu machen, sollte man vielleicht genauer sagen, wie die Definition im Skript gemeint ist: Rechts vom $:\Leftrightarrow$ sind $C,u,x,y$ existentiell gebunden und $x$ und $y$ wohl implizit verschieden.
D.h., Wenn du $C,u,x,y$ gegeben hast mit $s = C[\lambda x.u], t = C[\lambda y.u[y/x]], y \notin FV(u)$, also Daten für $s \to_\alpha t$, musst du Daten für $t \to_\alpha s$ finden, also $C',u',x',y'$ ($x'$, $y'$ verschieden) mit
$t = C'[\lambda x'.u'], s = C'[\lambda y'.u'[y'/x']], y'\notin FV(u')$.
Hier bietet sich wahrscheinlich an: $C'=C, y'=x, x'=y, u'=u[y/x]$.
Wenn dir das jedenfalls gelingt, hast du $\forall s,t.\, s \to_\alpha t \implies t \to_\alpha s$, woraus dann mit einem Induktionsbeweis $\forall s,t.\, s =_\alpha t \implies t =_\alpha s$ folgt (und der Beweis geht für beliebige Relationen: wenn $R$ symmetrisch, ist $R^*$ symmetrisch).\(\endgroup\)
|
Profil
|
DerTSH
Junior
Dabei seit: 09.12.2022
Mitteilungen: 14
| Beitrag No.2, vom Themenstarter, eingetragen 2023-04-01
|
Danke für Dein Feedback!
Wenn ich mich an den Beweis der Symmetrie begebe und $s \to_\alpha t \implies t \to_\alpha s$ zeige, dann würde ich mich auf Lemma 1.1.5 (2) aus dem Script stützen, das $s[t/x] = s$ falls $x \notin FV(s)$ - hier ist $t$ ein Term und $x$ eine Variable, die Ungleichheit $t \ne x$ wird dann wahrscheinlich vorausgesetzt?
Ich würde dann $x \ne y$ als weitere Voraussetzung mit einbringen und hätte darüber hinaus $x \notin FV(u)$ und $y \notin FV(u)$
Dann habe ich:
$s \to_\alpha t$ mit $s = C[\lambda x.u] \land t = C[\lambda y.(u[y/x])]$
dann möchte ich $t \to_\alpha s$ zeigen
und mache dies mit Substitution für $s$: $s = C[\lambda x.(u[x/y])]$
und für $t$: $t = C[\lambda y.(u[y/x][x/y])]$
für $t$ folgt dann $t = C[\lambda y.u]$
und insgesamt $t \to_\alpha s$ mit $t = C[\lambda y.u] \land s = C[\lambda x.(u[x/y])$
Fragezeichen. :)
|
Profil
|
tactac
Senior
Dabei seit: 15.10.2014
Mitteilungen: 2796
| Beitrag No.3, eingetragen 2023-04-01
|
\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]}
\newcommand{\name}[1]{\ulcorner#1\urcorner}
\newcommand{\upamp}{\mathbin {⅋}}
\newcommand{\monus}{\mathbin {∸}}\)
\quoteon(2023-04-01 21:37 - DerTSH in Beitrag No. 2)
Danke für Dein Feedback!
Wenn ich mich an den Beweis der Symmetrie begebe und $s \to_\alpha t \implies t \to_\alpha s$ zeige, dann würde ich mich auf Lemma 1.1.5 (2) aus dem Script stützen, das $s[t/x] = s$ falls $x \notin FV(s)$ - hier ist $t$ ein Term und $x$ eine Variable, die Ungleichheit $t \ne x$ wird dann wahrscheinlich vorausgesetzt?
\quoteoff
Nein, bei der Substitutionsdefinition wird das nicht vorausgesetzt.
Bei der Definition von $s \to_\alpha t$ ist $x \ne y$ implizit drin, weil es sich in der Formulierung um ganz konkrete Variablen handelt, die offensichtlich verschieden sind, die Metavariablen, über die *eigentlich* quantifiziert wird, könnten zufälligerweise denselben Namen enthalten, und man müsste dann explizit ein $\ne$ angeben. Im Skript wird eine Kurzform verwendet (die eben auch das Weglassen des eigentlich vorhandenen $\exists $ umfasst).
\quoteon
Ich würde dann $x \ne y$ als weitere Voraussetzung mit einbringen und hätte darüber hinaus $x \notin FV(u)$ und $y \notin FV(u)$
\quoteoff
$x \ne y$ ist ok. Du hast aus $s \to_\alpha t$ aber nur $y \notin FV(u)$ gegeben. $y' \notin FV(u')$ (was mit meinem Vorschlag $x \notin FV(u[y/x])$ ist) musst du *beweisen*, um $t \to_\alpha s$ zu zeigen.
\quoteon
Dann habe ich:
$s \to_\alpha t$ mit $s = C[\lambda x.u] \land t = C[\lambda y.(u[y/x])]$
dann möchte ich $t \to_\alpha s$ zeigen
und mache dies mit Substitution für $s$: $s = C[\lambda x.(u[x/y])]$
und für $t$: $t = C[\lambda y.(u[y/x][x/y])]$
für $t$ folgt dann $t = C[\lambda y.u]$
und insgesamt $t \to_\alpha s$ mit $t = C[\lambda y.u] \land s = C[\lambda x.(u[x/y])$
Fragezeichen. :)
\quoteoff
Ganz langsam!
Du hast $s \to_\alpha t$ gegeben durch $s = C[\lambda x.u] \land t = C[\lambda y.u[y/x]] \land y \notin FV(u)$
Du willst zeigen: $t \to_\alpha s$, dazu musst du für irgendwelche $C',x',y',u'$ zeigen: $t = C'[\lambda x'.u'] \land s = C'[\lambda y'.u'[y'/x']]\land y' \notin FV(u')$.
Mit den in #1 vorgeschlagenen $C',x',y',u'$ musst du also zeigen:
$t = C[\lambda y.u[y/x]] \land s = C[\lambda x.u[y/x][x/y]]\land x \notin FV(u[y/x])$.
\(\endgroup\)
|
Profil
|
DerTSH
Junior
Dabei seit: 09.12.2022
Mitteilungen: 14
| Beitrag No.4, vom Themenstarter, eingetragen 2023-04-02
|
Hey @tactac
\quoteon
dazu musst du für irgendwelche $C',x',y',u'$ zeigen
\quoteoff
Ich glaube, ich muß ein wenig umstellen. Wenn ich folgendes beweisen will:
Sei $s, t$ Term mit $s = \lambda x.u$ und $t = \lambda y.(u[y/x])$, und seien $x, y$ Variablen mit $x, y \notin FV(u)$ und $x \ne y$.
Zeige: Wenn $s \to_\alpha t$ gilt, dann gilt auch $t \to_\alpha s$.
Durch die Einschränkung kann ich den Beweis dann doch so durchführen, wie in meinem vorherigen Post, oder nicht? Ich habe dann klare Voraussetzungen geschaffen ($C$ ebenfalls entfernt) und Elemente, die ich für die Beweisführung benutzen kann.
|
Profil
|
tactac
Senior
Dabei seit: 15.10.2014
Mitteilungen: 2796
| Beitrag No.5, eingetragen 2023-04-02
|
\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]}
\newcommand{\name}[1]{\ulcorner#1\urcorner}
\newcommand{\upamp}{\mathbin {⅋}}
\newcommand{\monus}{\mathbin {∸}}\)
Das ergibt so keinen Sinn. Unter deinen Voraussetzungen hast du $s = \lambda x. u$ und $t = \lambda y. u$ (und $x,y \notin FV(u)$). $s \to_\alpha t \implies t \to_\alpha s$ gilt damit trivialerweise.
Lies dir #3 nochmal ganz aufmerksam durch. Und beweise einfach mal, was ich am Ende zum Beweis gestellt habe.\(\endgroup\)
|
Profil
|
| DerTSH hat die Antworten auf ihre/seine Frage gesehen. |
|
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2023 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die
Nutzungsbedingungen,
die Distanzierung,
die Datenschutzerklärung und das Impressum.
[Seitenanfang]
|
Home / Seite ohne Frame
Wie unterstütze ich den Matheplaneten mit Geld?
