Church-Rosser-Theorem Beispiel in einer funktionalen Programmiersprache

Question

Ich habe mehrere Referenzen auf die Church Rosser theorem, und insbesondere die Diamant-Eigenschaft Diagramm, beim Lernen funktionale Programmierung gesehen, aber ich bin nicht auf eine große Code-Beispiel gestoßen.

Wenn eine Sprache wie Haskell als eine Art Lambda-Kalkül betrachtet werden kann, dann muss es möglich sein, einige Beispiele mit der Sprache selbst zu trommeln.

Ich würde Bonuspunkte geben, wenn das Beispiel einfach zeigte, wie die Schritte oder Reduktionen zu leicht parallelisierbaren Ausführung führen.

Answer 1

All dieser Satz besagt, dass ein Ausdruck, der über mehrere Pfade reduziert werden kann, notwendigerweise weiter auf ein gemeinsames Produkt reduziert werden kann.

Nehmen wir zum Beispiel dieses Stück Haskell-Code:

vecLenSq :: Float -> Float -> Float 
vecLenSq x y = 
    xsq + ysq 
    where 
    xsq = x * x 
    ysq = y * y 

in Lambda Calculus Diese Funktion ist in etwa äquivalent zu (Pars hinzugefügt zur Klarheit, Operatoren primitive angenommen):

λ x . (λ y . (λ xsq . (λ ysq . (xsq + ysq)) (y * y)) (x * x)) 

The Die Expression kann reduziert werden, indem man zuerst eine β-Reduktion auf xsq anwendet oder indem man eine β-Reduktion auf ysq anwendet, dh die "Reihenfolge der Auswertung" ist willkürlich. Man kann den Ausdruck in der folgenden Reihenfolge reduzieren:

λ x . (λ y . (λ xsq . (xsq + (y * y))) (x * x)) 
λ x . (λ y . ((x * x) + (y * y))) 

... oder in der folgenden Reihenfolge:

λ x . (λ y . (λ ysq . ((x * x) + ysq)) (y * y)) 
λ x . (λ y . ((x * x) + (y * y))) 

Das Ergebnis ist offenbar gleich.

Dies bedeutet, dass die Begriffe xsq und ysq unabhängig reduzierbar sind und dass ihre Reduktionen parallelisiert werden können. Und in der Tat könnte man die Kürzungen wie so in Haskell parallelisieren:

vecLenSq :: Float -> Float -> Float 
vecLenSq x y = 
    (xsq `par` ysq) `pseq` xsq + ysq 
    where 
    xsq = x * x 
    ysq = y * y 

Diese Parallelisierung in Wirklichkeit würde keinen Vorteil in dieser besonderen Situation bieten, da zwei einfache Schwimmer Multiplikationen nacheinander ausgeführt ist effizienter als zwei paralellized Multiplikationen, weil von Planungs-Overhead, aber es könnte sich für komplexere Vorgänge lohnen.