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: (VP)
λxy.yx

Right? Seems like half-S-combinator.
juan_gandhi: (VP)


(10x [livejournal.com profile] _hacid_)

The list of references starts with Penrose.

author's page
juan_gandhi: (VP)
Дал им "дополнительную домашку" - выразить next succ в лямбде через комбинаторы.

Вот их ответ:

S(K (S ( S(KS) ( S(KK)I ) ) )) ( S ( S (KS) ( S(K(S(KS))) ( S ( KS)( S(KK)( S(KS)( S(KK)I) ))) (K (S(KK)I )))) ) (K (KI) ) )
juan_gandhi: (VP)
http://pchiusano.github.io/2014-06-12/extensible-dsls.html

P.Chiusano, "A very simple technique for making DSLs extensible"
juan_gandhi: (Default)
src
interface Lam<X, Y> {
  Y apply(X x);
}
 
// http://en.wikipedia.org/wiki/SKI_combinator_calculus
class SKI {
  public static <A, B, C> Lam<Lam<A, Lam<B, C>>, Lam<Lam<A, B>, Lam<A, C>>> s() {
    return new Lam<Lam<A, Lam<B, C>>, Lam<Lam<A, B>, Lam<A, C>>>() {
      public Lam<Lam<A, B>, Lam<A, C>> apply(final Lam<A, Lam<B, C>> f) {
        return new Lam<Lam<A, B>, Lam<A, C>>() {
          public Lam<A, C> apply(final Lam<A, B> g) {
            return new Lam<A, C>() {
              public C apply(final A a) {
                return f.apply(a).apply(g.apply(a));
              }
            };
          }
        };
      }
    };
  }
 
  public static <A, B> Lam<A, Lam<B, A>> k() {
    return new Lam<A, Lam<B, A>>() {
      public Lam<B, A> apply(final A a) {
        return new Lam<B, A>() {
          public A apply(final B b) {
            return a;
          }
        };
      }
    };
  }
 
  public static <A> Lam<A, A> i() {
    return SKI.<A, Lam<A, A>, A>s().apply(SKI.<A, Lam<A, A>>k()).apply(SKI.<A, A>k());
  }
}

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:42 am
Powered by Dreamwidth Studios