I believe I may have found a way to describe #zettelkasten work in #lambdacalculus — like, what it entails to do something in your Zettelkasten, and the communication system that emerges
Recent searches
Search options
#lambdacalculus
2 posts2 participants0 posts today
Lamber, my #LambdaCalculus -> Lisp compiler (https://github.com/aartaka/lamber) didn't handle big enough numbers (> 10-bit,) so I decided to implement some optimizations, reusing underlying #CommonLisp compiler to speed up and save space on numerics. It's not particularly reliable, because big LC numbers consume too much of the stack, but at least it's better than it used to be, almost reliably handling 12-bit numbers.
GitHubGitHub - aartaka/lamber: A functional scripting language compiling to pure Lambda CalculusA functional scripting language compiling to pure Lambda Calculus - aartaka/lamber
#python lets ypu instantiate a function anywhere and a ( recursive) function definition can be self contained and last i checked its notorious for its type checking
#Lambdacalculus wont let you do that unyil you give it the required fixed point function
#typetheory
Oh and fixed point need not be in R
Unlike rieman zeta ?
OTOH python wont spit potential Nonsense
term Q = λ1((λ11)(λλλλλ14(3(55)2)))1 concatenates two copies of its input, proving that
KS(xx) ≤ ℓ(x) + 66Applying it to its own encoding gives a 132 bit quine:
U(blc(Q) blc(Q) : Nil) = blc(Q) blc(Q)
#lambdacalculus
https://tromp.github.io/cl/Binary_lambda_calculus.html
!
> Forsp: A #Forth+#Lisp Hybrid #LambdaCalculus Language
https://xorvoid.com/forsp.html
xorvoid.comxorvoid
C-c-c-conjecturing, and dealing with recursion in Emacs (more excursus)
Another blog post, this one not tagged as part of the lambda-calculus series because it doesn't directly deal with lambda-calculus, but it follows on from Part 2, dealing with issues of recursion, and building up towards the #YCombinator and other #lambdacalculus issues.
Some fun things evaluating the efficiency of implementing different functions in #Elisp (with metrics!), and some fun images/visualisations of an interesting function.
In the spirit of (not-that-radical, unfortunately) openness (inspired by none other than @TodePond,) let me share a thing I've been quietly working on for the last couple of months: #Lamber, my pure #LambdaCalculus -compiling #FunctionalProgramming language inspired by #Lua and #haskell
Readings shared February 22, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/22-readings_shared_02-22-25 #LambdaCalculus #Lisp #Emacs
Vestigium · Readings shared February 22, 2025The readings shared in Bluesky on 22 February 2025 are
Lambda calculus and Lisp, part 1. #LambdaCalculus #Lisp
Lambda calculus and Lisp, part 2. #LambdaCalculus #Emacs #Lisp
Lambda calculus and Lisp, part 2. https://babbagefiles.xyz/lambda-calculus-and-lisp-02-recursion/ #LambdaCalculus #Emacs #Lisp
babbagefiles.xyz · Lambda Calculus and Lisp, part 2 (recursion excursion)From the previous entry in this series, one of the things of note in discussing the nature of the connections between LISP and (the) lambda calculus was John McCarthy’s concern about recursion and higher-order functions.
A couple of excerpts from previous quotes from McCarthy on the subject to set the stage:
…And so, the way in which to [be able to handle function passing/higher order functions] was to borrow from Church’s Lambda Calculus, to borrow the lambda definition.
Lambda calculus and Lisp, part 1. https://babbagefiles.xyz/lambda-calculus-and-lisp-01/ #LambdaCalculus #Lisp
babbagefiles.xyz · Lambda Calculus and Lisp, part 1The first of a series of envisioned blog posts on lambda calculus, and Lisp. It’s unclear exactly where to start: there is a whole heap of interesting issues, both theoretical and in terms of concrete implementations, which tangle and interconnect.
A particular application of lambda calculus is a very salient part of my “day job” as a formal semanticist of natural language. And my interests in Emacs and lisp(s) feel like they tie in here as well—though that’s a question in itself which is probably as good of a starting point into this (planned) series of posts as any.
The first of a planned series of posts on #Lisp and #LambdaCalculus and their connections:
Lambda Calculus and Lisp, part 1
"Did John McCarthy understand lambda calculus?"
Readings shared February 16, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/16-readings_shared_02-16-25 #CategoryTheory #FunctionalProgramming #Haskell #LLMs #LambdaCalculus #Logic #Reasoning
Vestigium · Readings shared February 16, 2025The readings shared in Bluesky on 16 February 2025 are
The relationship between category theory, lambda calculus, and functional programming in Haskell. ~ Antonio Montano. #Haskell #FunctionalProgram
The relationship between category theory, lambda calculus, and functional programming in Haskell. ~ Antonio Montano. https://4m4.it/posts/category-theory-functional-programming-compositionality/ #Haskell #FunctionalProgramming #CategoryTheory #LambdaCalculus
Random Bits of KnowledgeThe Relationship Between Category Theory, Lambda Calculus, and Functional Programming in Haskell – Random Bits of KnowledgeThis post explores the deep connections between functional programming, lambda calculus, and category theory, with a particular focus on composability, a foundational principle in both mathematics and software engineering. Haskell, a functional programming language deeply rooted in these mathematical frameworks, serves as the practical implementation of these concepts, demonstrating how abstract theories can be applied to build robust, scalable, and maintainable software systems. We present key concepts such as function composition, functors, monads, and cartesian closed categories, illustrating their significance in modern software development. Additionally, it highlights how formal composability, grounded in lambda calculus and category theory, is crucial for managing the growing complexity of software systems. The discussion extends to the future implications of formal composability in the context of machine learning and automated software development, emphasizing its potential to transform the way complex systems are designed and verified. Finally, the essay provides a comprehensive self-study path for those interested in mastering Haskell, category theory, and their applications in various domains, including secure coding, asynchronous systems, and blockchain technology.
#TIL that there's a #LambdaCalculus based language called brujin (for obvious reasons) and that it's absolutely unreadable! The standard library and the amount of work that went into it is extremely impressive though, so go give it a read:
https://bruijn.marvinborner.de/
and show some love to Marvin Borner, the creator of brujin!
I'm stealing parts of it (like Maybe monad) into #Lamber, my own applicative #LambdaCalculus compiling #Lua like language.
bruijn.marvinborner.debruijn programming languageFunctional programming language based on pure de Bruijn indexed lambda calculus.
What’s a good introduction to the Lambda calculus that you’ve personally used to learn? I wasn’t exposed to it in undergrad and need to understand wtf de Bruijn indices are in the moderately imminent future.
Y'all, how readable does this piece of code seem to you?
def div = fn (numer denom)
local loop = fn quot
when lt quot denom
then 0
else : succ : loop : sub quot denom
end
loop numer
end
That's division via subtraction from #Lamber standard library. And yes, it parses, compiles to pure #LambdaCalculus and returns the right number when applied properly!
Lamber (the WIP name of the language I'm making) compiles and runs factorial program:
let true = fn (t e) t
let false = fn (t e) e .
let iszero = fn (n)
n (fn x false) true .
let pred = fn (n f x)
n (fn (g h) h (g f))
(fn u x) (fn u u) .
let mult = fn (m n f) m (n f) .
let fac = fn : n
when : iszero n
then 1
else : mult n : fac : pred n
fac 6
Just so you know: Lamber is a #Lua, #Haskell, and #Wisp-inspired functional language compiling to pure #LambdaCalculus. And it's close to functioning well enough!
The asymmetry between "take" and "drop" #functionalProgramming operations on lists is weird. "drop" is just applying "cdr" N times, which is just a couple of function calls in #LambdaCalculus. While "take" requires full-blown #recursion and conditional testing. Or am I doing it wrong?