Entry tags:
Dana Scott's talk
Guys, I was writing notes; now I'm trying to decrypt them and format.
This is part one. Feel free to correct me, to ask questions, etc.
There are two more parts.
I was listening and writing down.
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:
similarly
How about
Composition combinator
Removing variables:
Traditional notation for
Some combinations don't stop rewriting themselves.
(only machines can read the result) - but it's
What if your combination consists only of
Expressions that have normal form form a set which is recursively enumerable, but not recursive.
Rules:
(I asked him about ξ - what's the universe over which the quantifier runs. Answer: "Good question!")
This 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.
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=JHow about
SKS? also JComposition 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.ASII combinator - it's self-application; leads to Russell paradox
ToC[(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 it
SS[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!")