bump lambda calculus examples

This commit is contained in:
Stephen Diehl 2015-12-10 10:55:42 -05:00
parent 142b1628a9
commit 133c1d82af
4 changed files with 80 additions and 9 deletions

View File

@ -400,6 +400,23 @@ In later variations of the lambda calculus let expressions will have different
semantics and will differ from applied lambda expressions. More on this will be
discussed in the section on Hindley-Milner inference.
Everything Can Be a $\lambda$ term
----------------------------------
* 0
* 1
* 2
* succ
* pred
* not
* and
* or
* add
* mul
Recursion
---------
@ -407,23 +424,29 @@ Probably the most famous combinator is Curry's Y combinator. Within an untyped
lambda calculus, Y can be used to allow an expression to contain a reference to
itself and reduce on itself permitting recursion and looping logic.
$$\textbf{Y} = \lambda f.(\lambda x.(f (x x)) \lambda x.(f (x x)))$$
$$
f = \textbf{YR}
$$
The Y combinator satisfies:
The $\textbf{Y}$ combinator is one of many so called fixed point combinators.
$$\textbf{Y} f = f (\textbf{Y} f) $$
$$
\textbf{Y} = \lambda R.(\lambda x.(R (x x)) \lambda x.(R (x x)))
$$
since
The combinator Y is called the fixed point combinator. Given R It returns the
fixed point of R.
$$
\begin{aligned}
\textbf{Y} f & = (\lambda f.(\lambda x.(f(x x)) \lambda x.(f(x x)))) f
& = (\lambda x.(f(x x))) (\lambda x.(f(x x)))
& = f((\lambda x.(f (x x))) (\lambda x.(f (x x))))
& = f(\textbf{Y} f)
\textbf{YR} &= \lambda f.(\lambda x.(f (x x)) \lambda x.(f (x x))) R \\
& = (\lambda x.(\textbf{R} (x x)) \lambda x.(\textbf{R} (x x))) \\
& = \textbf{R} (\lambda x.(\textbf{R} (x x)) \lambda x.(\textbf{R} (x x))) \\
& = \textbf{R Y R}
\end{aligned}
$$
For fun one can prove that the Y-combinator can be expressed in terms of the S
and K combinators.

View File

@ -9,6 +9,17 @@ To compile and run:
$ cabal run
```
Example
-------
```bash
Untyped> (\x. x) 1
=> \x . x
=> 1
=> x
1
```
License
=======

View File

@ -0,0 +1,37 @@
# For more information, see: https://github.com/commercialhaskell/stack/blob/release/doc/yaml_configuration.md
# Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2)
resolver: ghc-7.8.4
# Local packages, usually specified by relative directory name
packages:
- '.'
# Packages to be pulled from upstream that are not in the resolver (e.g., acme-missiles-0.3)
extra-deps:
- mtl-2.1.3.1
- parsec-3.1.9
- text-1.2.1.3
# Override default flag values for local packages and extra-deps
flags:
text:
integer-simple: false
# Extra package databases containing global packages
extra-package-dbs: []
# Control whether we use the GHC we find on the path
# system-ghc: true
# Require a specific version of stack, using version ranges
# require-stack-version: -any # Default
# require-stack-version: >= 0.1.4.0
# Override the architecture used by stack, especially useful on Windows
# arch: i386
# arch: x86_64
# Extra directories used by stack for building
# extra-include-dirs: [/path/to/dir]
# extra-lib-dirs: [/path/to/dir]

View File

@ -10,7 +10,7 @@ cabal-version: >=1.10
executable untyped
build-depends:
base >= 4.6 && <4.7
base >= 4.6 && <4.8
, pretty >= 1.1 && <1.2
, parsec >= 3.1 && <3.2
, containers >= 0.5 && <0.6