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

June 2025

S M T W T F S
1 2345 67
891011121314
15161718192021
22232425262728
2930     

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jun. 7th, 2025 06:36 am
Powered by Dreamwidth Studios