образованцы в роли литературных критиков

ailev.livejournal.com/1350731.html

Dana Scott's talk

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

цитата

"и розовые руки розовели из розовых коротких рукавов"