Light
Christian TietzeI 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
Artyom BologovLamber, 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.
coucou
What is PLUS times PLUS?
HoldMyType#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
#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
Csepp 🌢
!
(mapcar #'emacsomancer objs)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.
C-c-c-conjecturing, and dealing with recursion in Emacs (more excursus)
I’m not putting this in the lambda-calculus series, though it touches on issues from the last post in the series, but specifically issues of recursion. I was curious to go back and recall how The Little Schemer dealt with problems of recursion (and the Y Combinator (which we still haven’t got properly to yet, but we will, I promise)). In Chapter 9 of The Little Schemer (“and Again, and Again, and Again,…"), it starts off by querying the reader if they want caviar and how to find it in a list, and then essentially gets (from caviar and grits) into issues around the halting problem.
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
José A. AlonsoReadings shared February 22, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/22-readings_shared_02-22-25 #LambdaCalculus #Lisp #Emacs
