projects
/
matthijs
/
master-project
/
report.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
222070c
)
Add note about β-reduction for type variables.
author
Matthijs Kooijman
<matthijs@stdin.nl>
Tue, 1 Dec 2009 10:12:27 +0000
(11:12 +0100)
committer
Matthijs Kooijman
<matthijs@stdin.nl>
Tue, 1 Dec 2009 10:17:36 +0000
(11:17 +0100)
Chapters/Normalization.tex
patch
|
blob
|
history
diff --git
a/Chapters/Normalization.tex
b/Chapters/Normalization.tex
index 55e00577e393dc0c3933ecb708ad4c394d95ca5c..cdd57bb9c52da6a0d885ae2cadf02d114f76f548 100644
(file)
--- a/
Chapters/Normalization.tex
+++ b/
Chapters/Normalization.tex
@@
-812,6
+812,11
@@
sure that most lambda abstractions will eventually be reducable by
β-reduction.
sure that most lambda abstractions will eventually be reducable by
β-reduction.
+ Note that β-reduction also works on type lambda abstractions and type
+ applications as well. This means the substitution below also works on
+ type variables, in the case that the binder is a type variable and teh
+ expression applied to is a type.
+
\starttrans
(λx.E) M
-----------------
\starttrans
(λx.E) M
-----------------
@@
-829,6
+834,17
@@
\transexample{beta}{β-reduction}{from}{to}
\transexample{beta}{β-reduction}{from}{to}
+ \startbuffer[from]
+ (λt.λa::t. a) @Int
+ \stopbuffer
+
+ \startbuffer[to]
+ (λa::Int. a)
+ \stopbuffer
+
+ \transexample{beta-type}{β-reduction for type abstractions}{from}{to}
+
+
\subsubsection{Empty let removal}
This transformation is simple: It removes recursive lets that have no bindings
(which usually occurs when unused let binding removal removes the last
\subsubsection{Empty let removal}
This transformation is simple: It removes recursive lets that have no bindings
(which usually occurs when unused let binding removal removes the last