lists in Lambda in JavaScript
Dec. 31st, 2023 07:11 pm(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)) 
Option in JavaScript, funny lambda style
Dec. 30th, 2023 06:22 pm// 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))
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))
всякая примитивная лямбда
Nov. 16th, 2023 11:35 amDefining 
You can try it with
It will produce
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
[●●] [●●●] [] [●●]
Goodstein, Hydra, a question
Nov. 12th, 2019 09:58 pmhttp://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?)
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?)
a bunch of links
Mar. 10th, 2019 08:12 am Geometric Model Theory - hard reading, manifolds, algebraic geometry
Model Theory and Category Theory - high level, but easy reading
A link to the author's github project
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
nice reading
Dec. 9th, 2018 12:57 pmhttp://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.
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.
вопрос хаскельщикам
Apr. 20th, 2018 06:35 pmtrue 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?
фигня какая-то
Feb. 11th, 2018 10:13 amСтал искать, где бы понадыбать приятных теорем про CCC. Обнаружил, что а) CCC вообще никого не интересует, а интересует типизированный лямбда-калкулюс (хоть Барендрегта читай; который? Curry?) и б) единственная ссылка везде - это С.Соловьев, 1983. Я когда-то полагал, что Соловьев, конечно, классную тему поднял, но это было сильно по мотивам статейки Маклейна. А теперь Маклейна все забыли (ну только что в книге есть), а только Соловьев. Соловьева еле нашел, его даже на википедии нету; слава те господи, он в Тулузе, лямбду преподает в университете. Неплохо бы, конечно, заскочить к нему летом, если удастся.
Фигня какая-то получается. Посмотрю, какие из "аксиом CCC" следуют из ее категорного определения. Ну и BCCC, наверно, тоже надо впендюрить будет.
Но для меня сюрприз, что CCC - это чисто софтверное (или логическое) понятие.
И кстати, только что узнал, что CAML означает "categorical abstract machine language". Имея в виду ту же типизированную лямбду.
Фигня какая-то получается. Посмотрю, какие из "аксиом CCC" следуют из ее категорного определения. Ну и BCCC, наверно, тоже надо впендюрить будет.
Но для меня сюрприз, что CCC - это чисто софтверное (или логическое) понятие.
И кстати, только что узнал, что CAML означает "categorical abstract machine language". Имея в виду ту же типизированную лямбду.
Dana Scott's talk
Jun. 3rd, 2017 05:55 pmPart 2
axiomatizing lambda
we have α, β, η (will drop η somehow)
But is it consistent?
Algebraic Query Language (AQL) based on CT
Using Gödel numbering
-  pairing (n, m) = 2n*(2m+1)
-  sequences <> = 0, <n0,...nk> = (<n0,,, nk-1>, nk
-  Sets set(0) = {}, set((n, m)) = set(n) ∪ {m}
-  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
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)



![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)

