juan_gandhi: (Default)

Part 2



axiomatizing lambda



we have α, β, η (will drop η somehow)

But is it consistent?

Algebraic Query Language (AQL) based on CT

Using Gödel numbering

  1. pairing (n, m) = 2n*(2m+1)

  2. sequences <> = 0, <n0,...nk> = (<n0,,, nk-1>, nk

  3. Sets set(0) = {}, set((n, m)) = set(n) ∪ {m}

  4. Kleene star X* = {n | set{n} ⊂ X}, for sets X ⊂ ℕ



The universe is the powerset of integers



Definition Primitive recursive functions are those generated from the following: constant, projection, successor, by composition and simple recursion
    f(0, x) = g(x)
    f(n+1, x) = h(n, x, f(n, x))


Definition Recursively enumerable (RE) sets: those of the form {m |∃ n.p(n) = m+1} where p is primitive recursive.

Powerset of Integers



1) P(ℕ) is a topological space, {X | n ∊ X*} form a basis



2) CONTINUOUS FUNCTION Φ:P(ℕ)n → P(ℕ) if for all m ∊ ℕ, m ∊ Φ(x0, x1, ...)* iff there are ki ∊ X* for each i<n such that m ∊ Φ(set(k0), set(k1), ..., set(kn-1)) - "finite subset of function value information is determined by finite amount of information about the arguments"



3) APPLICATION OPERATION
Application F(X) = {m | ∃ n ∊ X* (n, m) ∊ F }



4) ABSTRACTION
Abstraction λ X.p...X... = {0} ∪ {(n, m) | m ∊ [... set(n)...]}
This {0} is here to ensure that it is the largest such set of numbers, 0 is not needed actually.



Application operator F(X) is continuous in both arguments (F and X)

Easy to prove (he says).

* If Φ(X0, X1, ..., Xn-1) is continuous, λ X0.Φ(X0,...Xn-1) is continuous on all remaining variables
* If Φ(X) is continuous, λ X. Φ(X) is the largest set F such that for all sets T, F(T) = Φ(T). Therefore, generally, F ⊂ λ X. F(X)

(draws picture, how open sets look like)

Complement function is not continuous (e.g. Russell set)

Theorem. For all sets of ints F and G,
    λ X.F(X) ⊂ λ X.G(X) iff ∀ X. F(X) ⊂ G(X)
    λX.(F(X) ∩ G(X)) = λ X.F(X) ∩ λ X.G(X)

same for union
juan_gandhi: (Default)
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.

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=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 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!")

Profile

juan_gandhi: (Default)
juan_gandhi

July 2017

S M T W T F S
       1
2 3 4 5 67 8
9 10 11 1213 14 15
16 17 18 19 20 21 22
23 24 2526272829
3031     

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 26th, 2017 04:44 am
Powered by Dreamwidth Studios