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