crossslink chapter 10

This commit is contained in:
Stephen Diehl 2015-12-12 13:42:06 -05:00
parent d0c03bb085
commit 041b118c5d
3 changed files with 28 additions and 12 deletions

View File

@ -37,6 +37,22 @@ names:
- **Lam** - A lambda abstraction
- **App** - An application
A lambda term is said to bind its variable. For example the lambda here binds
$x$. In mathematics we would typically write:
$$
f(x) = e
$$
Using the lambda calculus notation we write:
$$
f = \lambda x. e
$$
In other words, $\lambda x.e$ is a function that takes a variable $x$ and
returns $e$.
$$
\begin{aligned}
e :=\ & x & \trule{Var} \\
@ -52,13 +68,6 @@ Standard ML, etc. The variation we will discuss first is known as **untyped
lambda calculus**, by contrast later we will discuss the **typed lambda
calculus** which is an extension thereof.
A lambda abstraction is said to bind its variable.
For example the lambda here binds $x$.
$$
\lambda x. e
$$
There are several syntactical conventions that we will adopt when writing lambda
expressions. Application of multiple expressions associates to the left.
@ -149,8 +158,8 @@ This fact is a useful sanity check when testing an implementation of the lambda
**Omega Combinator**
An important degenerate case that we'll test is the omega combinator which applies a single argument to
itself.
An important degenerate case that we'll test is the omega combinator which
applies a single argument to itself.
$$
\omega = \lambda x. x x \\
@ -446,6 +455,13 @@ $$
\end{aligned}
$$
$$
n! = n (n-1)!
$$
$$
\textbf{fac}\ n = \textbf{R}(\textbf{fac}) = \textbf{R}(\textbf{R}(\textbf{fac}))
$$
For fun one can prove that the Y-combinator can be expressed in terms of the S
and K combinators.

View File

@ -35,8 +35,8 @@ Likewise for the product there are two function ``fst`` and ``snd`` which are
*projections* which de construct products.
```haskell
fst :: (a,b) -> a
snd :: (a,b) -> b
fst :: a * b -> a
snd :: a * b -> b
```
Once a language is endowed with the capacity to write a single product or a

View File

@ -37,7 +37,7 @@ Releases
* [Chapter 7: Hindley-Milner Inference](http://dev.stephendiehl.com/fun/006_hindley_milner.html)
* [Chapter 8: Design of ProtoHaskell](http://dev.stephendiehl.com/fun/007_path.html)
* [Chapter 9: Extended Parser](http://dev.stephendiehl.com/fun/008_extended_parser.html)
* Chapter 10: Custom Datatypes
* [Chapter 10: Custom Datatypes](http://dev.stephendiehl.com/fun/009_datatypes.html)
* Chapter 11: Renamer
* Chapter 12: Pattern Matching & Desugaring
* Chapter 13: System-F