### Dana Scott's talk

May. 31st, 2017 07:17 pmThis is part one. Feel free to correct me, to ask questions, etc.

There are two more parts.

## Introducing Lambda Calculus via Combinators

### Dana Scott's talk at LambdaConf 2017

*I was listening and writing down.*

Slides are made in Mathematica, in the form of Notebook.

Slides are made in Mathematica, in the form of Notebook.

A question from 100 years ago: "Is it possible to have a type-free theory of functions, where no difference is made between operators and arguments?"

A solution found by a crazy Russian at Göttingen (Moses Iljitsch Schônfinkel).

Somehow Haskell Curry was there too, doing his PhD.

*(now we know where he got it)*

Church reformulated Russell paradox using functions, not sets.

Church's son-in-law asked him once: "Dear professor Church, why did you have lambda for your operator?"

There's a paper by Hindley, "History of Lambda-calculus and Combinatory Logic"

(Mathematica uses square brackets for application)

Combinators names:

`I`

(or `J`

) for Identity, `K`

for Constant, `S`

stands for **Schönfinkel**!!!

crules = (J[x_] -> x, S[x_][y_][z_] -> x[z][y[z]], K[x_][y_]- > x); comb=J test=comb[A] crules test = test /. crules --------> A

similarly

`comb=S[K][K]`

and see that `SKK=J`

How about

`SKS`

? also `J`

Composition combinator

`S[K[S]][K]`

Removing variables:

ToC[vars_, comb_] := Fold[rm, comb, Reverse[vars]]; rm[x_, x_] := J rm[f_[v_], v{] /; FreeQ(f, v) := f; rm[h_, v_] /; FreeQ[h, v] := K[h]; rm[f_[g_], v_] := S[rm(f, v][rm[g, v] ]

Traditional notation for

`ToC[(x,y,z), A]`

is `λx.λy.λz.A`

`SII`

combinator - it's self-application; leads to Russell paradoxToC[(x,y,z), F[x][y][z] test=S[K[S[F]][K][x]y][z]

Some combinations don't stop rewriting themselves.

comb = ToC[(x), F[x[x]]] S[K[F]][S[J][J]][x] test = comb[comb]

(only machines can read the result) - but it's

`F[original combination]`

// is it a Y?What if your combination consists only of

`K`

? `K[K[K[K]]]][x][y][z]`

// did not get itSS[0] := S SS[n_] = SS[n-1][S] SS[2][SS[2]][SS[2]]

Expressions that have normal form form a set which is recursively enumerable, but not recursive.

#### traditional typeless lambda

Rules:

(α) (β) (η) (ξ) ∀ x [...x...] = [---x---] => λX[...X...] = λX[---X---]

(I asked him about ξ - what's the universe over which the quantifier runs. Answer: "Good question!")