Interestingly, in MARSQWEGES -> MARSCHWEGES, but not in WASCHBBSCH (WASQBUSQ)
2,373 karma · joined July 22, 2023
[0] https://news.ycombinator.com/item?id=40390287
[0]: https://en.wikipedia.org/wiki/Youth_word_of_the_year_(German...
> Claude may have some functional version of emotions or feelings
> [..] questions about Claude’s moral status, welfare, and consciousness remain deeply uncertain.
> It's a strange feeling to admire the cleverness of something I did and can't remember doing.
[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...
(responsible for the famous single-file C libraries)
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
α-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...
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...
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.
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.
[0]: https://bruijn.marvinborner.de/std/Number_Tuple.bruijn.html
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
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.
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.
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.
For example:
Other pages also contain some more advanced details and casestudies on effect handling
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...