juan_gandhi: (Default)
Фотки с конференции, где я языком чешу про лямбду. 
juan_gandhi: (Default)
(disclaimer: this is educational material)

  // Definitions for Boolean Logic
  const True  = x => y => x
  const False = x => y => y
  const Bool = b => b ? True : False

  // Definitions for pair and projection
  const p1 = x => y => x // did you notice? It's True
  const p2 = x => y => y // did you notice? It's False
  const Pair = x => y => f => f(x)(y)

  // Option constructors
  const None = Pair(True)("None")
  const Some = x => Pair(False)(x)

  // List constructors and operations
  const Nil = Pair(True)("Nil")
  const isEmpty = x => x(p1)
  const Head = z => z(p2)(p1)
  const HeadOption = z => z(p1)(None)(Some(z(p2)(p1)))
  const Tail = z => z(p2)(p2)
 
  const Cons = h => t => Pair(False)(Pair(h)(t))
  const Map = z => f => (isEmpty(z) (() => Nil) (() => Cons(f(Head(z))) (Map(Tail(z))(f))))()

  // visualizer

  const show = text => xs => {
    var buf = ""
    Map(xs)(x => buf += (x + ":"))
    println(`${text} ${buf}Nil`)
  }

  const Filter  = z => p =>
     (isEmpty(z) 
       (() => Nil) 
       (() => (p(Head(z)) (Cons(Head(z))(Filter(Tail(z))(p))) (Filter(Tail(z))(p))))
      )() // have to do it lazily

  // samples
  const ab = Cons("a")(Cons("b")(Nil))

  show("Expecting Nil ->")(Nil)
  show("Expecting a:b:Nil ->")(ab)

  const list1 = Cons(1)(Cons(-2)(Cons(3)(Cons(-4)(Nil))))

  show("three numbers")(list1)
  const isPositive = x => Bool(x > 0)

  show("squares")(Map(list1)(x => x*x))
  show("positives")(Filter(list1)(isPositive)) 

juan_gandhi: (Default)
// Definitions for Boolean Logic
const True = x => y => x
const False = x => y => y
const Bool = b => b ? True : False

// Definitions for pair and projection
const p1 = x => y => x // did you notice? It's True
const p2 = x => y => y // did you notice? It's False
const Pair = x => y => f => f(x)(y)

// Option constructors and operations
const None = Pair(True)("None")
const Some = x => Pair(False)(x)
const isEmpty = x => x(p1)
const FlatMap = x => f => isEmpty(x) (None) ( f(x(p2)))
const Map = x => f => isEmpty(x) (None) (Some(f(x(p2))))
const Filter = x => p => isEmpty(x) (None) (p(x(p2)) (x) (None))

// visualizer
const show = text => xOpt => {
Map(xOpt)(x => println(text + x))
}

// samples
show("Expecting Some ")(Some(42))
show("Expecting None ")(None)

const isPositive = x => Bool(x > 0)
show("0 positive? ")(Filter(Some(0))(isPositive))
show("2 positive? ")(Filter(Some(2))(isPositive))

const dec = n => n > 10 ? Some(n-10) : None

show("expecting None from None: ")(FlatMap( None)(dec))
show("expecting None from 5: ") (FlatMap(Some(5) )(dec))
show("expecting 32 from 42: ") (FlatMap(Some(42))(dec))
juan_gandhi: (Default)
Defining pred function in Church-encoded numbers in lambda:

  const _0 = f => x => x                   // zero, Church-encoded
  const succ = n => f => x =>f(n(f)(x))    // successor operation
  const p1 = x => y => x                   // first projection
  const p2 = x =>y => y                    // second projection
  const pair = x => y => f => f(x)(y)      // 'pair' function
  const p_0_0 = pair(_0)(_0)               // (0, 0)

  const pred = n => n(p => f => f(p(p2))(succ(p(p2))))(p_0_0)(p1)


You can try it with

  const _1 = succ(_0)              // number 1
  const _2 = succ(succ(_0))        // number 2
  const _3 = succ(succ(succ(_0)))  // number 3

  function print(n) {                   // show number 'n'
    const dot = s => "\\u25CF" + s      // as dots in square brackets
    console.log("[" + n(dot)("") + "]")
  }

  print(_2)         // we will see two dots
  print(_3)         // we will see three dots
  print(pred(_0))   // we will see no dots
  print(pred(_3))   // we will see two dots



It will produce

[●●]
[●●●]
[]
[●●]

now what

Jun. 4th, 2020 04:49 pm
juan_gandhi: (Default)

Evaluation order, it's all about initial or "final" "algebras", right? That's about Eilenberg-Moore category and Kleisli category.

Which, incidentally, are initial and terminal objects in the category of adjunctions producing the same monad.

Oh my. 

juan_gandhi: (Default)
http://math.andrej.com/2008/02/02/the-hydra-game/

My question actually is this: can Goodstein sequence to be proven to stop in a lambda calculus? Naively, it should be.

And another question: can set theory be modeled in lambda? (Or should I reread Dana Scott's works?)
juan_gandhi: (Default)
 Geometric Model Theory - hard reading, manifolds, algebraic geometry
Model Theory and Category Theory - high level, but easy reading

Solving the mystery behind Abstract Algorithm’s magical optimizations - here the author implements, in lambda, algorithms with unusually fast performance. Explanations follow (links inside)


A link to the author's github project





juan_gandhi: (Default)
http://www.ps.uni-saarland.de/courses/sem-ws17/confluence.pdf 

We study confluence of abstract relations and an abstract λβ-calculus parameterized with a function for β-reduction. We show confluence of the abstract λβ-calculus using parallel reduction and a Takahashi function. We also study evaluation, strong normalization, and uniform confluence.
juan_gandhi: (Default)
 
 
ι = λf (fS)K
 
I = ιι
K = ι(ι(ιι))
S = ι(ι(ι(ιι)))

src

juan_gandhi: (Default)
true x y = x
false x y = y

lampair :: a -> b -> (a -> b -> c) -> c
lampair x y p = p x y

pa :: ((a -> b -> c) ->c) -> a
pa p = p true


And I see
   • Couldn't match type ‘a’ with ‘c’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          pa :: forall a b c. ((a -> b -> c) -> c) -> a
        at sample1.hs:8:1-30
      ‘c’ is a rigid type variable bound by
        the type signature for:
          pa :: forall a b c. ((a -> b -> c) -> c) -> a
        at sample1.hs:8:1-30
      Expected type: a -> b -> c
        Actual type: c -> b -> c
    • In the first argument of ‘p’, namely ‘true’
      In the expression: p true
      In an equation for ‘pa’: pa p = p true
    • Relevant bindings include
        p :: (a -> b -> c) -> c (bound at sample1.hs:9:4)
        pa :: ((a -> b -> c) -> c) -> a (bound at sample1.hs:9:1)
  |


What have I done wrong? What fails here? Is Hindley-Milner "not smart enough"? What am I missing?
juan_gandhi: (Default)
Стал искать, где бы понадыбать приятных теорем про CCC. Обнаружил, что а) CCC вообще никого не интересует, а интересует типизированный лямбда-калкулюс (хоть Барендрегта читай; который? Curry?) и б) единственная ссылка везде - это С.Соловьев, 1983. Я когда-то полагал, что Соловьев, конечно, классную тему поднял, но это было сильно по мотивам статейки Маклейна. А теперь Маклейна все забыли (ну только что в книге есть), а только Соловьев. Соловьева еле нашел, его даже на википедии нету; слава те господи, он в Тулузе, лямбду преподает в университете. Неплохо бы, конечно, заскочить к нему летом, если удастся.

Фигня какая-то получается. Посмотрю, какие из "аксиом CCC" следуют из ее категорного определения. Ну и BCCC, наверно, тоже надо впендюрить будет.

Но для меня сюрприз, что CCC - это чисто софтверное (или логическое) понятие.

И кстати, только что узнал, что CAML означает "categorical abstract machine language". Имея в виду ту же типизированную лямбду.


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) ) )

Profile

juan_gandhi: (Default)
Juan-Carlos Gandhi

October 2025

S M T W T F S
    1 23 4
5 678 9 1011
12 13 1415 161718
1920 2122 23 2425
26 2728 293031 

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Oct. 31st, 2025 02:52 am
Powered by Dreamwidth Studios