close

Anmelden

Neues Passwort anfordern?

Anmeldung mit OpenID

Freie Theoreme — Was und Wie - Janis Voigtländer

EinbettenHerunterladen
Freie Theoreme — Was und Wie
(Haskell in Leipzig 3)
Janis Voigtl¨ander
Technische Universit¨
at Dresden
18. April 2008
Ein Beispiel:
filter :: (α → Bool) → [α] → [α]
filter p [ ]
= []
filter p (x : xs) = if p x then x : filter p xs else filter p xs
2
Ein Beispiel:
filter :: (α → Bool) → [α] → [α]
filter p [ ]
= []
filter p (x : xs) = if p x then x : filter p xs else filter p xs
Behauptung:
filter p (map h l) = map h (filter (p ◦ h) l)
Kann per Induktion u
¨ber l bewiesen werden.
2
Ein Beispiel:
filter :: (α → Bool) → [α] → [α]
filter p [ ]
= []
filter p (x : xs) = if p x then x : filter p xs else filter p xs
Behauptung:
filter p (map h l) = map h (filter (p ◦ h) l)
Kann per Induktion u
¨ber l bewiesen werden.
¨
Ahnlich
gilt:
takeWhile p (map h l) = map h (takeWhile (p ◦ h) l)
2
Ein Beispiel:
Behauptung:
filter p (map h l) = map h (filter (p ◦ h) l)
Kann per Induktion u
¨ber l bewiesen werden.
¨
Ahnlich
gilt:
takeWhile p (map h l) = map h (takeWhile (p ◦ h) l)
Tats¨achlich gilt f¨
ur jedes f :: (α → Bool) → [α] → [α],
f p (map h l) = map h (f (p ◦ h) l)
2
Ein Beispiel:
Behauptung:
filter p (map h l) = map h (filter (p ◦ h) l)
Kann per Induktion u
¨ber l bewiesen werden.
¨
Ahnlich
gilt:
takeWhile p (map h l) = map h (takeWhile (p ◦ h) l)
Tats¨achlich gilt f¨
ur jedes f :: (α → Bool) → [α] → [α],
f p (map h l) = map h (f (p ◦ h) l)
Zauberei? Keine Induktion mehr n¨otig?
2
Ein Beispiel:
Behauptung:
filter p (map h l) = map h (filter (p ◦ h) l)
Kann per Induktion u
¨ber l bewiesen werden.
¨
Ahnlich
gilt:
takeWhile p (map h l) = map h (takeWhile (p ◦ h) l)
Tats¨achlich gilt f¨
ur jedes f :: (α → Bool) → [α] → [α],
f p (map h l) = map h (f (p ◦ h) l)
Zauberei? Keine Induktion mehr n¨otig?
Freie Theoreme! [Wadler 1989]
2
Warum? (intuitiv)
f :: (α → Bool) → [α] → [α] muss f¨
ur jede m¨ogliche
Instanziierung von α einheitlich arbeiten.
3
Warum? (intuitiv)
f :: (α → Bool) → [α] → [α] muss f¨
ur jede m¨ogliche
Instanziierung von α einheitlich arbeiten.
Die Ausgabeliste kann nur Elemente der Eingabe l enthalten.
3
Warum? (intuitiv)
f :: (α → Bool) → [α] → [α] muss f¨
ur jede m¨ogliche
Instanziierung von α einheitlich arbeiten.
Die Ausgabeliste kann nur Elemente der Eingabe l enthalten.
Welche, und in welcher Reihenfolge/Vielfachheit, kann
lediglich von l und dem Eingabepr¨adikat p abh¨angen.
3
Warum? (intuitiv)
f :: (α → Bool) → [α] → [α] muss f¨
ur jede m¨ogliche
Instanziierung von α einheitlich arbeiten.
Die Ausgabeliste kann nur Elemente der Eingabe l enthalten.
Welche, und in welcher Reihenfolge/Vielfachheit, kann
lediglich von l und dem Eingabepr¨adikat p abh¨angen.
Die einzig m¨oglichen Grundlagen zur Entscheidung sind die
L¨ange von l und die Ergebnisse von p auf Elementen von l.
3
Warum? (intuitiv)
f :: (α → Bool) → [α] → [α] muss f¨
ur jede m¨ogliche
Instanziierung von α einheitlich arbeiten.
Die Ausgabeliste kann nur Elemente der Eingabe l enthalten.
Welche, und in welcher Reihenfolge/Vielfachheit, kann
lediglich von l und dem Eingabepr¨adikat p abh¨angen.
Die einzig m¨oglichen Grundlagen zur Entscheidung sind die
L¨ange von l und die Ergebnisse von p auf Elementen von l.
Aber, die Listen (map h l) und l haben stets die selbe L¨ange.
3
Warum? (intuitiv)
f :: (α → Bool) → [α] → [α] muss f¨
ur jede m¨ogliche
Instanziierung von α einheitlich arbeiten.
Die Ausgabeliste kann nur Elemente der Eingabe l enthalten.
Welche, und in welcher Reihenfolge/Vielfachheit, kann
lediglich von l und dem Eingabepr¨adikat p abh¨angen.
Die einzig m¨oglichen Grundlagen zur Entscheidung sind die
L¨ange von l und die Ergebnisse von p auf Elementen von l.
Aber, die Listen (map h l) und l haben stets die selbe L¨ange.
Und Anwendung von p auf ein Element von (map h l) hat
stets das selbe Ergebnis wie Anwendung von (p ◦ h) auf das
entsprechende Element von l.
3
Warum? (intuitiv)
f :: (α → Bool) → [α] → [α] muss f¨
ur jede m¨ogliche
Instanziierung von α einheitlich arbeiten.
Die Ausgabeliste kann nur Elemente der Eingabe l enthalten.
Welche, und in welcher Reihenfolge/Vielfachheit, kann
lediglich von l und dem Eingabepr¨adikat p abh¨angen.
Die einzig m¨oglichen Grundlagen zur Entscheidung sind die
L¨ange von l und die Ergebnisse von p auf Elementen von l.
Aber, die Listen (map h l) und l haben stets die selbe L¨ange.
Und Anwendung von p auf ein Element von (map h l) hat
stets das selbe Ergebnis wie Anwendung von (p ◦ h) auf das
entsprechende Element von l.
Also w¨ahlt f mit p stets die selben“ Elemente aus (map h l)
”
wie es f mit (p ◦ h) aus l tut,
3
Warum? (intuitiv)
f :: (α → Bool) → [α] → [α] muss f¨
ur jede m¨ogliche
Instanziierung von α einheitlich arbeiten.
Die Ausgabeliste kann nur Elemente der Eingabe l enthalten.
Welche, und in welcher Reihenfolge/Vielfachheit, kann
lediglich von l und dem Eingabepr¨adikat p abh¨angen.
Die einzig m¨oglichen Grundlagen zur Entscheidung sind die
L¨ange von l und die Ergebnisse von p auf Elementen von l.
Aber, die Listen (map h l) und l haben stets die selbe L¨ange.
Und Anwendung von p auf ein Element von (map h l) hat
stets das selbe Ergebnis wie Anwendung von (p ◦ h) auf das
entsprechende Element von l.
Also w¨ahlt f mit p stets die selben“ Elemente aus (map h l)
”
wie es f mit (p ◦ h) aus l tut, außer dass im ersten Fall die
entsprechenden Abbilder unter h ausgegeben werden.
3
Warum? (intuitiv)
f :: (α → Bool) → [α] → [α] muss f¨
ur jede m¨ogliche
Instanziierung von α einheitlich arbeiten.
Die Ausgabeliste kann nur Elemente der Eingabe l enthalten.
Welche, und in welcher Reihenfolge/Vielfachheit, kann
lediglich von l und dem Eingabepr¨adikat p abh¨angen.
Die einzig m¨oglichen Grundlagen zur Entscheidung sind die
L¨ange von l und die Ergebnisse von p auf Elementen von l.
Aber, die Listen (map h l) und l haben stets die selbe L¨ange.
Und Anwendung von p auf ein Element von (map h l) hat
stets das selbe Ergebnis wie Anwendung von (p ◦ h) auf das
entsprechende Element von l.
Also w¨ahlt f mit p stets die selben“ Elemente aus (map h l)
”
wie es f mit (p ◦ h) aus l tut, außer dass im ersten Fall die
entsprechenden Abbilder unter h ausgegeben werden.
Also ist (f p (map h l)) gleich (map h (f (p ◦ h) l)).
3
Warum? (intuitiv)
f :: (α → Bool) → [α] → [α] muss f¨
ur jede m¨ogliche
Instanziierung von α einheitlich arbeiten.
Die Ausgabeliste kann nur Elemente der Eingabe l enthalten.
Welche, und in welcher Reihenfolge/Vielfachheit, kann
lediglich von l und dem Eingabepr¨adikat p abh¨angen.
Die einzig m¨oglichen Grundlagen zur Entscheidung sind die
L¨ange von l und die Ergebnisse von p auf Elementen von l.
Aber, die Listen (map h l) und l haben stets die selbe L¨ange.
Und Anwendung von p auf ein Element von (map h l) hat
stets das selbe Ergebnis wie Anwendung von (p ◦ h) auf das
entsprechende Element von l.
Also w¨ahlt f mit p stets die selben“ Elemente aus (map h l)
”
wie es f mit (p ◦ h) aus l tut, außer dass im ersten Fall die
entsprechenden Abbilder unter h ausgegeben werden.
Also ist (f p (map h l)) gleich (map h (f (p ◦ h) l)).
Genau das wollten wir beweisen!
3
Warum? (formaler, aber etwas naiv)
Frage: Welche f haben Typ ∀α. (α → Bool) → [α] → [α] ?
4
Warum? (formaler, aber etwas naiv)
Frage: Welche f haben Typ ∀α. (α → Bool) → [α] → [α] ?
Ansatz: Denotationen von Typen als Mengen angeben.
[[Bool]]
[[Int]]
= {True, False}
= {. . . , −2, −1, 0, 1, 2, . . . }
4
Warum? (formaler, aber etwas naiv)
Frage: Welche f haben Typ ∀α. (α → Bool) → [α] → [α] ?
Ansatz: Denotationen von Typen als Mengen angeben.
[[Bool]]
[[Int]]
[[(τ1 , τ2 )]]
[[[τ ]]]
=
=
=
=
{True, False}
{. . . , −2, −1, 0, 1, 2, . . . }
[[τ1 ]] × [[τ2 ]]
{[x1 , . . . , xn ] | n ≥ 0, xi ∈ [[τ ]]}
4
Warum? (formaler, aber etwas naiv)
Frage: Welche f haben Typ ∀α. (α → Bool) → [α] → [α] ?
Ansatz: Denotationen von Typen als Mengen angeben.
[[Bool]]
[[Int]]
[[(τ1 , τ2 )]]
[[[τ ]]]
[[τ1 → τ2 ]]
=
=
=
=
=
{True, False}
{. . . , −2, −1, 0, 1, 2, . . . }
[[τ1 ]] × [[τ2 ]]
{[x1 , . . . , xn ] | n ≥ 0, xi ∈ [[τ ]]}
{f : [[τ1 ]] → [[τ2 ]]}
4
Warum? (formaler, aber etwas naiv)
Frage: Welche f haben Typ ∀α. (α → Bool) → [α] → [α] ?
Ansatz: Denotationen von Typen als Mengen angeben.
[[Bool]]
[[Int]]
[[(τ1 , τ2 )]]
[[[τ ]]]
[[τ1 → τ2 ]]
[[∀α.τ ]]
=
=
=
=
=
=
{True, False}
{. . . , −2, −1, 0, 1, 2, . . . }
[[τ1 ]] × [[τ2 ]]
{[x1 , . . . , xn ] | n ≥ 0, xi ∈ [[τ ]]}
{f : [[τ1 ]] → [[τ2 ]]}
?
4
Warum? (formaler, aber etwas naiv)
Frage: Welche f haben Typ ∀α. (α → Bool) → [α] → [α] ?
Ansatz: Denotationen von Typen als Mengen angeben.
[[Bool]]
[[Int]]
[[(τ1 , τ2 )]]
[[[τ ]]]
[[τ1 → τ2 ]]
[[∀α.τ ]]
=
=
=
=
=
=
{True, False}
{. . . , −2, −1, 0, 1, 2, . . . }
[[τ1 ]] × [[τ2 ]]
{[x1 , . . . , xn ] | n ≥ 0, xi ∈ [[τ ]]}
{f : [[τ1 ]] → [[τ2 ]]}
?
g ∈ [[∀α. τ ]] m¨
usste eine ganze Familie“ von Werten sein:
”
f¨
ur jeden Typ τ , eine Instanz mit Typ τ [τ /α].
4
Warum? (formaler, aber etwas naiv)
Frage: Welche f haben Typ ∀α. (α → Bool) → [α] → [α] ?
Ansatz: Denotationen von Typen als Mengen angeben.
[[Bool]]
[[Int]]
[[(τ1 , τ2 )]]
[[[τ ]]]
[[τ1 → τ2 ]]
[[∀α.τ ]]
=
=
=
=
=
=
{True, False}
{. . . , −2, −1, 0, 1, 2, . . . }
[[τ1 ]] × [[τ2 ]]
{[x1 , . . . , xn ] | n ≥ 0, xi ∈ [[τ ]]}
{f : [[τ1 ]] → [[τ2 ]]}
?
g ∈ [[∀α. τ ]] m¨
usste eine ganze Familie“ von Werten sein:
”
f¨
ur jeden Typ τ , eine Instanz mit Typ τ [τ /α].
[[∀α.τ ]] = {g | ∀τ . gτ ∈ [[τ [τ /α]]]} ?
4
Warum? (formaler, aber etwas naiv)
Frage: Welche f haben Typ ∀α. (α → Bool) → [α] → [α] ?
Ansatz: Denotationen von Typen als Mengen angeben.
[[Bool]]
[[Int]]
[[(τ1 , τ2 )]]
[[[τ ]]]
[[τ1 → τ2 ]]
[[∀α.τ ]]
=
=
=
=
=
=
{True, False}
{. . . , −2, −1, 0, 1, 2, . . . }
[[τ1 ]] × [[τ2 ]]
{[x1 , . . . , xn ] | n ≥ 0, xi ∈ [[τ ]]}
{f : [[τ1 ]] → [[τ2 ]]}
?
g ∈ [[∀α. τ ]] m¨
usste eine ganze Familie“ von Werten sein:
”
f¨
ur jeden Typ τ , eine Instanz mit Typ τ [τ /α].
[[∀α.τ ]] = {g | ∀τ . gτ ∈ [[τ [τ /α]]]} ?
Aber das schließt ad-hoc-polymorphe“ Funktionen ein!
”
4
Unerw¨
unschte Ad-Hoc-Polymorphie am Beispiel
Mit der vorgeschlagenen Definition,
[[∀α. (α, α) → α]] = {g | ∀τ. gτ : [[τ ]] × [[τ ]] → [[τ ]]}.
5
Unerw¨
unschte Ad-Hoc-Polymorphie am Beispiel
Mit der vorgeschlagenen Definition,
[[∀α. (α, α) → α]] = {g | ∀τ. gτ : [[τ ]] × [[τ ]] → [[τ ]]}.
Aber das erlaubt auch
gBool (x, y ) = not x
gInt (x, y ) = y + 1 ,
was in Haskell beim Typ ∀α. (α, α) → α unm¨oglich ist.
5
Unerw¨
unschte Ad-Hoc-Polymorphie am Beispiel
Mit der vorgeschlagenen Definition,
[[∀α. (α, α) → α]] = {g | ∀τ. gτ : [[τ ]] × [[τ ]] → [[τ ]]}.
Aber das erlaubt auch
gBool (x, y ) = not x
gInt (x, y ) = y + 1 ,
was in Haskell beim Typ ∀α. (α, α) → α unm¨oglich ist.
Um dies zu vermeiden, m¨
ussen wir
gBool : [[Bool]] × [[Bool]] → [[Bool]] und
gInt : [[Int]] × [[Int]] → [[Int]]
vergleichen und gew¨ahrleisten, dass sie sich
identisch verhalten“.
”
5
Unerw¨
unschte Ad-Hoc-Polymorphie am Beispiel
Mit der vorgeschlagenen Definition,
[[∀α. (α, α) → α]] = {g | ∀τ. gτ : [[τ ]] × [[τ ]] → [[τ ]]}.
Aber das erlaubt auch
gBool (x, y ) = not x
gInt (x, y ) = y + 1 ,
was in Haskell beim Typ ∀α. (α, α) → α unm¨oglich ist.
Um dies zu vermeiden, m¨
ussen wir
gBool : [[Bool]] × [[Bool]] → [[Bool]] und
gInt : [[Int]] × [[Int]] → [[Int]]
vergleichen und gew¨ahrleisten, dass sie sich
identisch verhalten“.
”
Aber wie?
5
Idee [Reynolds 1983]
Beliebige Relationen benutzen, um Instanzen zu verkn¨
upfen!
6
Idee [Reynolds 1983]
Beliebige Relationen benutzen, um Instanzen zu verkn¨
upfen!
Im Beispiel (g :: ∀α. (α, α) → α):
Man w¨ahle eine Relation R ⊆ Bool × Int.
6
Idee [Reynolds 1983]
Beliebige Relationen benutzen, um Instanzen zu verkn¨
upfen!
Im Beispiel (g :: ∀α. (α, α) → α):
Man w¨ahle eine Relation R ⊆ Bool × Int.
Man nenne (x1 , x2 ) ∈ Bool × Bool und (y1 , y2 ) ∈ Int × Int
verwandt, wenn (x1 , y1 ) ∈ R und (x2 , y2 ) ∈ R.
6
Idee [Reynolds 1983]
Beliebige Relationen benutzen, um Instanzen zu verkn¨
upfen!
Im Beispiel (g :: ∀α. (α, α) → α):
Man w¨ahle eine Relation R ⊆ Bool × Int.
Man nenne (x1 , x2 ) ∈ Bool × Bool und (y1 , y2 ) ∈ Int × Int
verwandt, wenn (x1 , y1 ) ∈ R und (x2 , y2 ) ∈ R.
Man nenne f1 : Bool × Bool → Bool und f2 : Int × Int → Int
verwandt, wenn verwandte Eingaben zu verwandten Ausgaben
f¨
uhren.
6
Idee [Reynolds 1983]
Beliebige Relationen benutzen, um Instanzen zu verkn¨
upfen!
Im Beispiel (g :: ∀α. (α, α) → α):
Man w¨ahle eine Relation R ⊆ Bool × Int.
Man nenne (x1 , x2 ) ∈ Bool × Bool und (y1 , y2 ) ∈ Int × Int
verwandt, wenn (x1 , y1 ) ∈ R und (x2 , y2 ) ∈ R.
Man nenne f1 : Bool × Bool → Bool und f2 : Int × Int → Int
verwandt, wenn verwandte Eingaben zu verwandten Ausgaben
f¨
uhren.
Dann sind gBool und gInt mit
gBool (x, y ) = not x und
gInt (x, y ) = y + 1
nicht verwandt bei, zum Beispiel, Wahl von R = {(True, 1)}.
6
Idee [Reynolds 1983]
Beliebige Relationen benutzen, um Instanzen zu verkn¨
upfen!
Im Beispiel (g :: ∀α. (α, α) → α):
Man w¨ahle eine Relation R ⊆ Bool × Int.
Man nenne (x1 , x2 ) ∈ Bool × Bool und (y1 , y2 ) ∈ Int × Int
verwandt, wenn (x1 , y1 ) ∈ R und (x2 , y2 ) ∈ R.
Man nenne f1 : Bool × Bool → Bool und f2 : Int × Int → Int
verwandt, wenn verwandte Eingaben zu verwandten Ausgaben
f¨
uhren.
Dann sind gBool und gInt mit
gBool (x, y ) = not x und
gInt (x, y ) = y + 1
nicht verwandt bei, zum Beispiel, Wahl von R = {(True, 1)}.
Reynolds: g ∈ [[∀α.τ ]] genau dann wenn f¨
ur alle τ1 , τ2 und
R ⊆ [[τ1 ]] × [[τ2 ]] gilt, dass gτ1 und gτ2 verwandt per
Fortsetzung“ von R bez¨
uglich τ
”
6
Etwas genauer
Zur Interpretation von Typen als Relationen:
1. Ersetze (Quantifizierung u
¨ber) Typvariablen durch
(Quantifizierung ¨uber) Relationsvariablen.
7
Etwas genauer
Zur Interpretation von Typen als Relationen:
1. Ersetze (Quantifizierung u
¨ber) Typvariablen durch
(Quantifizierung ¨uber) Relationsvariablen.
2. Ersetze Teiltypen ohne jeglichen Polymorphismus durch
Identit¨atsrelationen.
7
Etwas genauer
Zur Interpretation von Typen als Relationen:
1. Ersetze (Quantifizierung u
¨ber) Typvariablen durch
(Quantifizierung ¨uber) Relationsvariablen.
2. Ersetze Teiltypen ohne jeglichen Polymorphismus durch
Identit¨atsrelationen.
3. Verwende folgende Regeln:
(R, S)
= {((x1 , x2 ), (y1 , y2 )) | (x1 , y1 ) ∈ R, (x2 , y2 ) ∈ S}
7
Etwas genauer
Zur Interpretation von Typen als Relationen:
1. Ersetze (Quantifizierung u
¨ber) Typvariablen durch
(Quantifizierung ¨uber) Relationsvariablen.
2. Ersetze Teiltypen ohne jeglichen Polymorphismus durch
Identit¨atsrelationen.
3. Verwende folgende Regeln:
(R, S)
= {((x1 , x2 ), (y1 , y2 )) | (x1 , y1 ) ∈ R, (x2 , y2 ) ∈ S}
[R]
= {([x1 , . . . , xn ], [y1 , . . . , yn ]) | n ≥ 0, (xi , yi ) ∈ R}
7
Etwas genauer
Zur Interpretation von Typen als Relationen:
1. Ersetze (Quantifizierung u
¨ber) Typvariablen durch
(Quantifizierung ¨uber) Relationsvariablen.
2. Ersetze Teiltypen ohne jeglichen Polymorphismus durch
Identit¨atsrelationen.
3. Verwende folgende Regeln:
(R, S)
= {((x1 , x2 ), (y1 , y2 )) | (x1 , y1 ) ∈ R, (x2 , y2 ) ∈ S}
[R]
= {([x1 , . . . , xn ], [y1 , . . . , yn ]) | n ≥ 0, (xi , yi ) ∈ R}
R→S
= {(f1 , f2 ) | ∀(a1 , a2 ) ∈ R. (f1 a1 , f2 a2 ) ∈ S}
7
Etwas genauer
Zur Interpretation von Typen als Relationen:
1. Ersetze (Quantifizierung u
¨ber) Typvariablen durch
(Quantifizierung ¨uber) Relationsvariablen.
2. Ersetze Teiltypen ohne jeglichen Polymorphismus durch
Identit¨atsrelationen.
3. Verwende folgende Regeln:
(R, S)
= {((x1 , x2 ), (y1 , y2 )) | (x1 , y1 ) ∈ R, (x2 , y2 ) ∈ S}
[R]
= {([x1 , . . . , xn ], [y1 , . . . , yn ]) | n ≥ 0, (xi , yi ) ∈ R}
R→S
= {(f1 , f2 ) | ∀(a1 , a2 ) ∈ R. (f1 a1 , f2 a2 ) ∈ S}
∀R. F(R) = {(u, v ) | ∀τ1 , τ2 , R ⊆ τ1 × τ2 . (uτ1 , vτ2 ) ∈ F(R)}
7
Etwas genauer
Zur Interpretation von Typen als Relationen:
1. Ersetze (Quantifizierung u
¨ber) Typvariablen durch
(Quantifizierung ¨uber) Relationsvariablen.
2. Ersetze Teiltypen ohne jeglichen Polymorphismus durch
Identit¨atsrelationen.
3. Verwende folgende Regeln:
(R, S)
= {((x1 , x2 ), (y1 , y2 )) | (x1 , y1 ) ∈ R, (x2 , y2 ) ∈ S}
[R]
= {([x1 , . . . , xn ], [y1 , . . . , yn ]) | n ≥ 0, (xi , yi ) ∈ R}
R→S
= {(f1 , f2 ) | ∀(a1 , a2 ) ∈ R. (f1 a1 , f2 a2 ) ∈ S}
∀R. F(R) = {(u, v ) | ∀τ1 , τ2 , R ⊆ τ1 × τ2 . (uτ1 , vτ2 ) ∈ F(R)}
Dann gilt f¨
ur jedes f :: τ , dass das Paar (f , f ) in der Interpretation
von τ als Relation enthalten ist.
7
Nun formal am Beispiel
Gegeben sei f :: ∀α. (α → Bool) → ([α] → [α]).
8
Nun formal am Beispiel
Gegeben sei f :: ∀α. (α → Bool) → ([α] → [α]).
Dann:
(f , f ) ∈ ∀R. (R → id Bool ) → ([R] → [R])
8
Nun formal am Beispiel
Gegeben sei f :: ∀α. (α → Bool) → ([α] → [α]).
Dann:
(f , f ) ∈ ∀R. (R → id Bool ) → ([R] → [R])
⇔ ∀τ1 , τ2 , R ⊆ τ1 × τ2 . (fτ1 , fτ2 ) ∈ (R → id Bool ) → ([R] → [R])
wegen Definition von ∀R. F(R)
8
Nun formal am Beispiel
Gegeben sei f :: ∀α. (α → Bool) → ([α] → [α]).
Dann:
(f , f ) ∈ ∀R. (R → id Bool ) → ([R] → [R])
⇔ ∀τ1 , τ2 , R ⊆ τ1 × τ2 . (fτ1 , fτ2 ) ∈ (R → id Bool ) → ([R] → [R])
⇔ ∀R. ∀(a1 , a2 ) ∈ (R → id Bool ). (fτ1 a1 , fτ2 a2 ) ∈ ([R] → [R])
wegen Definition von R → S
8
Nun formal am Beispiel
Gegeben sei f :: ∀α. (α → Bool) → ([α] → [α]).
Dann:
(f , f ) ∈ ∀R. (R → id Bool ) → ([R] → [R])
⇔ ∀τ1 , τ2 , R ⊆ τ1 × τ2 . (fτ1 , fτ2 ) ∈ (R → id Bool ) → ([R] → [R])
⇔ ∀R. ∀(a1 , a2 ) ∈ (R → id Bool ). (fτ1 a1 , fτ2 a2 ) ∈ ([R] → [R])
⇔ ∀R. ∀(a1 , a2 ) ∈ (R → id Bool ). ∀(l1 , l2 ) ∈ [R].
(fτ1 a1 l1 , fτ2 a2 l2 ) ∈ [R]
wegen Definition von R → S
8
Nun formal am Beispiel
Gegeben sei f :: ∀α. (α → Bool) → ([α] → [α]).
Dann:
(f , f ) ∈ ∀R. (R → id Bool ) → ([R] → [R])
⇔ ∀τ1 , τ2 , R ⊆ τ1 × τ2 . (fτ1 , fτ2 ) ∈ (R → id Bool ) → ([R] → [R])
⇔ ∀R. ∀(a1 , a2 ) ∈ (R → id Bool ). (fτ1 a1 , fτ2 a2 ) ∈ ([R] → [R])
⇔ ∀R. ∀(a1 , a2 ) ∈ (R → id Bool ). ∀(l1 , l2 ) ∈ [R].
(fτ1 a1 l1 , fτ2 a2 l2 ) ∈ [R]
⇒ ∀(a1 , a2 ) ∈ (h → id Bool ). ∀(l1 , l2 ) ∈ (map h).
(fτ1 a1 l1 , fτ2 a2 l2 ) ∈ (map h)
durch Spezialisierung zu R = h, wobei dann [R] = (map h)
f¨
ur jede Funktion h :: τ1 → τ2
8
Nun formal am Beispiel
Gegeben sei f :: ∀α. (α → Bool) → ([α] → [α]).
Dann:
(f , f ) ∈ ∀R. (R → id Bool ) → ([R] → [R])
⇔ ∀τ1 , τ2 , R ⊆ τ1 × τ2 . (fτ1 , fτ2 ) ∈ (R → id Bool ) → ([R] → [R])
⇔ ∀R. ∀(a1 , a2 ) ∈ (R → id Bool ). (fτ1 a1 , fτ2 a2 ) ∈ ([R] → [R])
⇔ ∀R. ∀(a1 , a2 ) ∈ (R → id Bool ). ∀(l1 , l2 ) ∈ [R].
(fτ1 a1 l1 , fτ2 a2 l2 ) ∈ [R]
⇒ ∀(a1 , a2 ) ∈ (h → id Bool ). ∀(l1 , l2 ) ∈ (map h).
(fτ1 a1 l1 , fτ2 a2 l2 ) ∈ (map h)
⇒ ∀(l1 , l2 ) ∈ (map h). (fτ1 (p ◦ h) l1 , fτ2 p l2 ) ∈ (map h)
durch Wahl von (a1 , a2 ) = (p ◦ h, p) ∈ (h → id Bool )
f¨
ur jede Funktion h :: τ1 → τ2 und jedes p :: τ2 → Bool.
8
Nun formal am Beispiel
Gegeben sei f :: ∀α. (α → Bool) → ([α] → [α]).
Dann:
(f , f ) ∈ ∀R. (R → id Bool ) → ([R] → [R])
⇔ ∀τ1 , τ2 , R ⊆ τ1 × τ2 . (fτ1 , fτ2 ) ∈ (R → id Bool ) → ([R] → [R])
⇔ ∀R. ∀(a1 , a2 ) ∈ (R → id Bool ). (fτ1 a1 , fτ2 a2 ) ∈ ([R] → [R])
⇔ ∀R. ∀(a1 , a2 ) ∈ (R → id Bool ). ∀(l1 , l2 ) ∈ [R].
(fτ1 a1 l1 , fτ2 a2 l2 ) ∈ [R]
⇒ ∀(a1 , a2 ) ∈ (h → id Bool ). ∀(l1 , l2 ) ∈ (map h).
(fτ1 a1 l1 , fτ2 a2 l2 ) ∈ (map h)
⇒ ∀(l1 , l2 ) ∈ (map h). (fτ1 (p ◦ h) l1 , fτ2 p l2 ) ∈ (map h)
⇔ ∀l1 :: [τ1 ]. map h (fτ1 (p ◦ h) l1 ) = fτ2 p (map h l1 )
durch einfache Umformung
f¨
ur jede Funktion h :: τ1 → τ2 und jedes p :: τ2 → Bool.
8
Nun formal am Beispiel
Gegeben sei f :: ∀α. (α → Bool) → ([α] → [α]).
Dann:
(f , f ) ∈ ∀R. (R → id Bool ) → ([R] → [R])
⇔ ∀τ1 , τ2 , R ⊆ τ1 × τ2 . (fτ1 , fτ2 ) ∈ (R → id Bool ) → ([R] → [R])
⇔ ∀R. ∀(a1 , a2 ) ∈ (R → id Bool ). (fτ1 a1 , fτ2 a2 ) ∈ ([R] → [R])
⇔ ∀R. ∀(a1 , a2 ) ∈ (R → id Bool ). ∀(l1 , l2 ) ∈ [R].
(fτ1 a1 l1 , fτ2 a2 l2 ) ∈ [R]
⇒ ∀(a1 , a2 ) ∈ (h → id Bool ). ∀(l1 , l2 ) ∈ (map h).
(fτ1 a1 l1 , fτ2 a2 l2 ) ∈ (map h)
⇒ ∀(l1 , l2 ) ∈ (map h). (fτ1 (p ◦ h) l1 , fτ2 p l2 ) ∈ (map h)
⇔ ∀l1 :: [τ1 ]. map h (fτ1 (p ◦ h) l1 ) = fτ2 p (map h l1 )
f¨
ur jede Funktion h :: τ1 → τ2 und jedes p :: τ2 → Bool.
Das entspricht genau der urspr¨
unglichen Behauptung!
8
Short Cut Fusion [Gill et al. 1993]
Beispiel:
fromTo n m = go n
where go i = if i > m then [ ]
else i : go (succ i)
sum [ ]
=0
sum (x : xs) = x + sum xs
9
Short Cut Fusion [Gill et al. 1993]
Beispiel:
fromTo n m = go n
where go i = if i > m then [ ]
else i : go (succ i)
sum [ ]
=0
sum (x : xs) = x + sum xs
Problem: Ausdr¨
ucke wie
sum (fromTo 1 10)
f¨
uhren zur Erzeugung eines Zwischenergebnisses.
9
Short Cut Fusion [Gill et al. 1993]
Beispiel:
fromTo n m = go n
where go i = if i > m then [ ]
else i : go (succ i)
sum [ ]
=0
sum (x : xs) = x + sum xs
Problem: Ausdr¨
ucke wie
sum (fromTo 1 10)
f¨
uhren zur Erzeugung eines Zwischenergebnisses.
L¨osung:
1. Schreibe fromTo mittels build.
2. Schreibe sum mittels foldr .
3. Benutze folgende Regel:
{−# RULES “foldr/build”
∀(g :: ∀β. (α → β → β) → β → β) c n.
foldr c n (build g ) = g c n
#−}
9
Korrektheitsbeweis
Zur Erinnerung:
build :: (∀β. (α → β → β) → β → β) → [α]
build g = g (:) [ ]
10
Korrektheitsbeweis
Zur Erinnerung:
build :: (∀β. (α → β → β) → β → β) → [α]
build g = g (:) [ ]
Gegeben sei g :: ∀β. (τ → β → β) → β → β.
10
Korrektheitsbeweis
Zur Erinnerung:
build :: (∀β. (α → β → β) → β → β) → [α]
build g = g (:) [ ]
Gegeben sei g :: ∀β. (τ → β → β) → β → β. Dann:
(g , g ) ∈ ∀R. (id τ → R → R) → (R → R)
10
Korrektheitsbeweis
Zur Erinnerung:
build :: (∀β. (α → β → β) → β → β) → [α]
build g = g (:) [ ]
Gegeben sei g :: ∀β. (τ → β → β) → β → β. Dann:
(g , g ) ∈ ∀R. (id τ → R → R) → (R → R)
⇔ ∀R. ∀(c1 , c2 ) ∈ (id τ → R → R). ∀(n1 , n2 ) ∈ R.
(gτ1 c1 n1 , gτ2 c2 n2 ) ∈ R
wegen Definition von ∀R. F(R) und R → S
10
Korrektheitsbeweis
Zur Erinnerung:
build :: (∀β. (α → β → β) → β → β) → [α]
build g = g (:) [ ]
Gegeben sei g :: ∀β. (τ → β → β) → β → β. Dann:
(g , g ) ∈ ∀R. (id τ → R → R) → (R → R)
⇔ ∀R. ∀(c1 , c2 ) ∈ (id τ → R → R). ∀(n1 , n2 ) ∈ R.
(gτ1 c1 n1 , gτ2 c2 n2 ) ∈ R
⇒
((:), c2 ) ∈ (id τ → (foldr c2 n2 ) → (foldr c2 n2 ))
∧ ([ ], n2 ) ∈ (foldr c2 n2 )
⇒ (g[τ ] (:) [ ], gτ c2 n2 ) ∈ (foldr c2 n2 )
durch Spezialisierung zu R = foldr c 2 n2 , c1 = (:) und n1 = [ ]
f¨
ur jede m¨ogliche Wahl von c2 :: τ → τ → τ und n2 :: τ .
10
Korrektheitsbeweis
Zur Erinnerung:
build :: (∀β. (α → β → β) → β → β) → [α]
build g = g (:) [ ]
Gegeben sei g :: ∀β. (τ → β → β) → β → β. Dann:
(g , g ) ∈ ∀R. (id τ → R → R) → (R → R)
⇔ ∀R. ∀(c1 , c2 ) ∈ (id τ → R → R). ∀(n1 , n2 ) ∈ R.
(gτ1 c1 n1 , gτ2 c2 n2 ) ∈ R
((:), c2 ) ∈ (id τ → (foldr c2 n2 ) → (foldr c2 n2 ))
⇒
∧ ([ ], n2 ) ∈ (foldr c2 n2 )
⇒ (g[τ ] (:) [ ], gτ c2 n2 ) ∈ (foldr c2 n2 )
⇔ foldr c2 n2 (g[τ ] (:) [ ]) = gτ c2 n2
durch Vereinfachung
f¨
ur jede m¨ogliche Wahl von c2 :: τ → τ → τ und n2 :: τ .
10
Korrektheitsbeweis
Zur Erinnerung:
build :: (∀β. (α → β → β) → β → β) → [α]
build g = g (:) [ ]
Gegeben sei g :: ∀β. (τ → β → β) → β → β. Dann:
(g , g ) ∈ ∀R. (id τ → R → R) → (R → R)
⇔ ∀R. ∀(c1 , c2 ) ∈ (id τ → R → R). ∀(n1 , n2 ) ∈ R.
(gτ1 c1 n1 , gτ2 c2 n2 ) ∈ R
⇒
((:), c2 ) ∈ (id τ → (foldr c2 n2 ) → (foldr c2 n2 ))
∧ ([ ], n2 ) ∈ (foldr c2 n2 )
⇒ (g[τ ] (:) [ ], gτ c2 n2 ) ∈ (foldr c2 n2 )
⇔ foldr c2 n2 (g[τ ] (:) [ ]) = gτ c2 n2
⇔ foldr c2 n2 (build g ) = gτ c2 n2
per Definition von build
f¨
ur jede m¨ogliche Wahl von c2 :: τ → τ → τ und n2 :: τ .
10
Korrektheitsbeweis
Zur Erinnerung:
build :: (∀β. (α → β → β) → β → β) → [α]
build g = g (:) [ ]
Gegeben sei g :: ∀β. (τ → β → β) → β → β. Dann:
(g , g ) ∈ ∀R. (id τ → R → R) → (R → R)
⇔ ∀R. ∀(c1 , c2 ) ∈ (id τ → R → R). ∀(n1 , n2 ) ∈ R.
(gτ1 c1 n1 , gτ2 c2 n2 ) ∈ R
⇒
((:), c2 ) ∈ (id τ → (foldr c2 n2 ) → (foldr c2 n2 ))
∧ ([ ], n2 ) ∈ (foldr c2 n2 )
⇒ (g[τ ] (:) [ ], gτ c2 n2 ) ∈ (foldr c2 n2 )
⇔ foldr c2 n2 (g[τ ] (:) [ ]) = gτ c2 n2
⇔ foldr c2 n2 (build g ) = gτ c2 n2
f¨
ur jede m¨ogliche Wahl von c2 :: τ → τ → τ und n2 :: τ .
10
Außerdem
weitere Fusion-Regeln:
destroy/unfoldr [Svenningsson 2002]
circular fusion [Fernandes et al. 2007]
stream fusion [Coutts et al. 2007]
...
11
Außerdem
weitere Fusion-Regeln:
destroy/unfoldr [Svenningsson 2002]
circular fusion [Fernandes et al. 2007]
stream fusion [Coutts et al. 2007]
...
Einbeziehung von Typ- und Typkonstruktorklassen
11
Außerdem
weitere Fusion-Regeln:
destroy/unfoldr [Svenningsson 2002]
circular fusion [Fernandes et al. 2007]
stream fusion [Coutts et al. 2007]
...
Einbeziehung von Typ- und Typkonstruktorklassen
0-1-k Prinzipien [Day et al. 1999, V. 2008]
...?
11
Literatur I
D. Coutts, R. Leshchinskiy, and D. Stewart.
Stream fusion: From lists to streams to nothing at all.
In International Conference on Functional Programming,
Proceedings, pages 315–326. ACM Press, 2007.
N.A. Day, J. Launchbury, and J. Lewis.
Logical abstractions in Haskell.
In Haskell Workshop, Proceedings. Technical Report
UU-CS-1999-28, Utrecht University, 1999.
J.P. Fernandes, A. Pardo, and J. Saraiva.
A shortcut fusion rule for circular program calculation.
In Haskell Workshop, Proceedings, pages 95–106. ACM Press,
2007.
12
Literatur II
A. Gill, J. Launchbury, and S.L. Peyton Jones.
A short cut to deforestation.
In Functional Programming Languages and Computer
Architecture, Proceedings, pages 223–232. ACM Press, 1993.
J.C. Reynolds.
Types, abstraction and parametric polymorphism.
In Information Processing, Proceedings, pages 513–523.
Elsevier Science Publishers B.V., 1983.
J. Svenningsson.
Shortcut fusion for accumulating parameters & zip-like
functions.
In International Conference on Functional Programming,
Proceedings, pages 124–132. ACM Press, 2002.
13
Literatur III
J. Voigtl¨ander.
Much ado about two: A pearl on parallel prefix computation.
In Principles of Programming Languages, Proceedings, pages
29–35. ACM Press, 2008.
P. Wadler.
Theorems for free!
In Functional Programming Languages and Computer
Architecture, Proceedings, pages 347–359. ACM Press, 1989.
14
Document
Kategorie
Kunst und Fotos
Seitenansichten
5
Dateigröße
216 KB
Tags
1/--Seiten
melden