HN user
marvinborner.de
Of course they get programmed, just not in the ordinary sense. Claude is trained using Anthropic's "constitution" [0] which importantly does not contain clear statements against consciousness/emotions. They even conclude these problems themself:
Claude may have some functional version of emotions or feelings
[..] questions about Claude’s moral status, welfare, and consciousness remain deeply uncertain.
I hate that Anthropic seemingly tries to make Claude act as if it was conscious or had feelings
It's a strange feeling to admire the cleverness of something I did and can't remember doing.
They are not functions, but variables. Maybe this helps, as they basically are "selectors": https://text.marvinborner.de/2024-11-18-00.html#tagged-union...
fwiw, one of the FFT challenges is about the Scott encoding [1], while the other uses Church trees at least [2]. Both use a balanced ternary numeral system, which is a lot more efficient than plain Church/Scott and fairly well-known [3]. Either way, I would have assumed there to be a chance that at least one of the AIs had a look at [4] -- a tutorial about FFT in LC by the benchmark creator himself.
[1] task: https://github.com/VictorTaelin/lambench/blob/main/tsk/stre_... solution: https://github.com/VictorTaelin/lambench/blob/main/lam/stre_...
[2] task: https://github.com/VictorTaelin/lambench/blob/main/tsk/ctre_... solution: https://github.com/VictorTaelin/lambench/blob/main/lam/ctre_...
[3] https://link.springer.com/chapter/10.1007/3-540-45575-2_20
[4] https://gist.github.com/VictorTaelin/5776ede998d0039ad1cc9b1...
You can inspect the point system in its source, `const questions = [...]`.
Sean Barret's website: https://nothings.org/
(responsible for the famous single-file C libraries)
Even UTC+-0 I have seen rarely. AoE seems more common, especially for deadlines
Quadtrees are also quite useful for generating fractals. A very related project of mine, Lambda Screen [0], explores this by encoding these functional quadtrees directly in lambda calculus and rendering the structure based on Church booleans being true (white) or false (black).
With fixed point recursion, this allows for very tiny definitions of IFS fractals. For example, fractals like the Sierpinski triangle/carpet only require ~50 bit of binary lambda calculus [1] [2]!
[0] https://text.marvinborner.de/2024-03-25-02.html
[1] https://lambda-screen.marvinborner.de/?term=ERoc0CrYLYA%3D
[2] https://lambda-screen.marvinborner.de/?term=QcCqqttsFtsI0OaA
The annihilating interaction between abstraction and application nodes is well-known in the area of interaction net research to ~correspond to β-reduction, as is also explained in the associated research paper [1].
α-conversion is not required in interaction nets. η-reduction is an additional rule not typically discussed, but see for example [2].
[1] https://arxiv.org/pdf/2505.20314
[2] https://www.sciencedirect.com/science/article/pii/S030439750...
While easy, it sadly doesn't preserve semantics.
There is actually an easy way that does preserve semantics at least to WHNF - it's called closed reduction. Mackie has worked on it a bunch (see some resources [1]).
An even simpler implementation is Sinot's token passing.
The problem with both of these approaches is the decreased amount of sharing and potential for parallelism, which is typically the reason for using interaction nets in the first place.
[1] https://github.com/marvinborner/interaction-net-resources?ta...
This is quite different. Salvadori's work aims for optimal reduction of the full lambda calculus (which requires something called "bookkeeping"/"oracle"), while HOC works on optimal/parallel reduction of a certain subset of the lambda calculus.
Both approaches have been researched for a long time now, where HOC's subset is typically referred to as "abstract algorithm". For example, a version of the lambdas calculus where any variable can be used at most once (the "affine lambda calculus"), can be reduced optimally with interaction nets without requiring any bookkeeping.
The novel thing about Salvadori's work is that it develops a new (and better explained) bookkeeping mechanism.
then the numbers should not be stored as Peano integers a.k.a. base 1 in the first place
That's my point though. The linked n-ary encoding by Mogensen, for example, does not suffer from such complexities. Depending on the reducer's implementation, (supported) operations on my presented de Bruijn numerals are also sublinear. I doubt 8-tuples of Church booleans would be efficient though - except when letting machine instructions leak into LC.
Though I agree that the focus of functional data structures should lie on embedded folds. Compared to nested Church pairs, folded Church tuples (\cons nil.cons a (cons b nil)) or Church n-tuples (\s.s a b c) should be preferred in many cases.
Thanks, added it to bruijn's standard library [0]. Looks like it has some very interesting properties!
[0] https://bruijn.marvinborner.de/std/Number_Tuple.bruijn.html
Scott-Mogensen encoding
just Scott encoding, Scott-Mogensen refers to a meta encoding of LC in LC. Scott's encoding is fine but requires fixpoint recursion for many operations as you said.
Interestingly though, Mogensen's ternary encoding [1] does not require fixpoint recursion and is the most efficient (wrt being compact) encoding in LC known right now.
Just use [..], seriously
do you have any further arguments for Scott's encoding? There are many number encodings with constant time predecessor, and with any number requiring O(n) space and `add` being this complex, it becomes quite hard to like
Good idea, I like "caramelized"!
However, I wouldn't define bruijn as being caramelized just yet. Personally, I view as syntactic sugar only syntax that's expanded to the target language by the parser/compiler. In bruijn's case, there is barely any of such syntax sugar aside of number/string/char encodings. Everything else is part of the infix/prefix/mixfix standard library definitions which get substituted as part of the translation to LC.
I don't know any quadtree/lowlevel encoding of LC that could be memoized like that. Though you could, for example, cache the reduction of any term by hash and substitute the matching hashes with its nf. This doesn't really work for lazy reducers or when you do not reduce strongly. And, of course (same as hashlife), this would use a lot of memory. With a lot more possibilities than GoL per "entity" (NxN grid vs variables/applications/abstractions), there will also be a lot more hash misses.
There's also graph encodings like interaction nets, which have entirely local reduction behavior. Compared to de Bruijn indices, bindings are represented by edges, which makes them more applicable to hash consing. I once spent some time trying to add this kind of memoization but there are some further challenges involved, unfortunately.
Or just (flip .), which also allows ((flip .) .) etc. for further flips.
In Smullyan's "To Mock a Mockingbird", these combinators are described as "cardinal combinator once/twice/etc. removed", where the cardinal combinator itself defines flip.
In recent years there has been a movement to collaborate on math proofs via blueprints (dependency graphs) in the Lean language, which seems related.
For example:
Regarding Effekt, here's an interactive introduction on how to use its effect system: https://effekt-lang.org/tour/effects
Other pages also contain some more advanced details and casestudies on effect handling
As a reference on the volume aspect: I have a tiny server where I host some of my git repos. After the fans of my server spun increasingly faster/louder every week, I decided to log the requests [1]. In a single week, ClaudeBot made 2.25M (!) requests (7.55GiB), whereas GoogleBot made only 24 requests (8.37MiB). After installing Anubis the traffic went down to before the AI hype started.
I think emiT [1] comes quite close!
A time paradox from [2]:
create x = 10;
time point;
print x; //prints 10 in first timeline, and 20 in the next
create traveler = 20;
traveler warps point{
x = traveler;
traveler kills traveler;
};
[2] https://www.reddit.com/r/ProgrammingLanguages/comments/1golf...
This should also include the chart on "Coding deception" [1] which is quite deceptive (50.0 is not in fact less than 47.4)
Reddit's r/programminglanguages is still quite active. Otherwise most of the community switched to Discord, it seems. (I found Par by hopping the Discord servers of "Programming Language Development"->HOC->Vine->Par)
Do you know about the Par language? They try to integrate Par into a usable syntax
It's interesting how some of these diagrams are almost equivalent in the context of encoding computation in interaction nets using symmetric interaction combinators [1].
From the perspective of the lambda calculus for example, the duplication of the addition node in "When Adding met Copying" [2] mirrors exactly the iterative duplication of lambda terms - ie. something like (λx.x x) M!
[1] https://ezb.io/thoughts/interaction_nets/lambda_calculus/202...
[2] https://graphicallinearalgebra.net/2015/05/12/when-adding-me...
There's a video by Hannah Cairo that explains the conjecture and her results [1]
Also, Terence Tao hinted at some further advances some time ago [2], does anyone know more about that?
Is this supposed to be a joke reflecting point (3)?
Also, once you get used to it, it makes writing large lambda terms faster, easier and more intuitive. The terms all just kind of magically interconnect in your mind after a while. At least that has been my experience after writing a lot of code in pure de Bruijn-indexed lambda calculus using bruijn [1]. Otherwise, thinking a few reduction steps ahead in complex terms requires alpha conversion, which often ends in confusion.
Similarly, it seems like languages with de Bruijn indices are immune to LLMs, since they require an internal stack/graph of sorts and don't reduce only on a textual basis.
Very cool! This basically encodes a quad-tree of bits where every except one quadrant of each subquadrant recurses on the parent quad-tree.
The corresponding equivalent of functional programming would be Church bits in a functional quad-tree encoding \s.(s TL TR BL BR). Then, the Sierpinski triangle can be written as (Y \fs.(s f f f #f)), where #f is the Church bit \tf.f!
Rendering proof: https://lambda-screen.marvinborner.de/?term=ERoc0CrbYIA%3D