Not logged in. · Lost password · Register

[hedgehogs dilemma = 42]
Member since Jan 2014
243 posts
Subject: Frage applikative Reduktion
Hallo Zusammen,

kann mir jemand beantworten ob folgende applikative Reduktion richtig wäre und wenn falsch wie Sie richtig ginge?

Applikative Reduktion nach Regeln der Vorlesung:
geq [2] [1] →  Regel 4  (delta)
geq λf a.f(f a) [1]  -> Regel 4  (delta)
geq  λf a.f(f a) λf b.f b->Regel 3 (delta)
isZero (λf a.f(f a) pred λf b.f b) ->Regel 3  (delta)
isZero (λf a.f(f a)  fst(λf b.f b ( λp.pair(snd p) (succ(snd p))) (pair [0] [0])))


Regeln für applikative Reduktion aus Vorlesung:
1.    (�λx. t)s ->a t[s/x], wenn t und s normal sind.
2.    λ�x. t ->a λ�x. t', wenn t ->a t'.
3.    ts ->a t's, wenn t ->a t' und s normal ist.
4.    ts ->a ts', wenn s ->a s'.
quaestor
Christoph Rauch, INF8
Avatar
Member since Sep 2007
98 posts
Hallo,
 
hier hat sich gleich mal ein Fehler im ersten Schritt eingeschlichen, Stichwort Klammerung. Siehe z.B. den Abschnitt "Zur Notation" auf Übungsblatt 4. Die letzte Umformung ist dann auch diesem Fehler zum Opfer gefallen. Am besten mal zur Übung explizit Klammern setzen!

Grüße
Christoph
Metal is like an apple, no one likes the core.
[hedgehogs dilemma = 42]
Member since Jan 2014
243 posts
wie hätte die umformung hier dann entsprechend aussehen müssen und wie sähen hier die klammern aus wenn man sie setzen würde?

ich  hatte gedacht, dass die applikative reduktion entsprechend von innen nach außen arbeitet und die argumente einer funktion zuerst ausgewertet werden - hier also [2] und [1]
Klammerung hätte ich gedacht wäre wie folgt geq ([2] [1])
quaestor
Christoph Rauch, INF8
Avatar
Member since Sep 2007
98 posts
Nein, die Klammerung ist eben (geq [2]) [1]. Denn ("Zur Notation", Übungsblatt 4):

Applikation ist links-assoziativ.
Beispielsweise kürzen wir ((x(yz))u)v zu x(yz)uv.

Ebenso ist dann in der vorletzten Zeile
((λf a.f(f a) pred) λf b.f b)
zu klammern.
Metal is like an apple, no one likes the core.
lemur
Member since Oct 2013
110 posts
War aber der Schritt richtig, dass zuerst die Definition von [2] eingesetzt wurde, oder hätte man zuerst [1] auflösen müssen?
[hedgehogs dilemma = 42]
Member since Jan 2014
243 posts
wäre folgende Reduktion entsprechend richtig?


geq [2] [1] →  Regel 4  (delta)
geq [2] λf b.f b  -> Regel 4  (delta)
geq  λf a.f(f a) λf b.f b ->Regel 3 (delta)
isZero (λf a.f(f a) pred λf b.f b) -> (beta)
isZero (λ a.pred(pred a)  λf b.f b)

welche Regel sollte beim letzen Schritt zum einsatz kommen?


Regeln für applikative Reduktion aus Vorlesung:
1.    (�λx. t)s ->a t[s/x], wenn t und s normal sind.
2.    λ�x. t ->a λ�x. t', wenn t ->a t'.
3.    ts ->a t's, wenn t ->a t' und s normal ist.
4.    ts ->a ts', wenn s ->a s'.
This post was edited on 2016-10-11, 13:50 by [hedgehogs dilemma = 42].
quaestor
Christoph Rauch, INF8
Avatar
Member since Sep 2007
98 posts
Die Aufgabe ist unterspezifiziert, deswegen kann es hier keine "richtige" Reduktion geben. Wie ist denn "geq" definiert? Es gibt hier mehrere Möglichkeiten:

geq = λn m . isZero (n pred m)
geq n = λm . isZero (n pred m)
geq n m = isZero (n pred m)

Siehe zu diesem Unterschied Übungsblatt 4, Aufgabe 2.2.
Metal is like an apple, no one likes the core.
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen