marvinborner

Do you know about the Par language? They try to integrate Par into a usable syntax

https://github.com/faiface/par-lang

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?

[1]: https://www.youtube.com/watch?v=3ZeH_8sTyKA

[2]: https://mathstodon.xyz/@tao/114003793236630744

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.

[1]: https://bruijn.marvinborner.de/

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

Yes, there are tutorials on how to do that. Takes only around 5 minutes apparently!

When encoding tagged unions as lambdas, the tags are arguments. In this case `Nothing` has two available tags (`nothing` and `just`) and uses the tag `nothing`. `Just` does the same with the tag `just`, only that the tag gets an additional argument (as does its constructor `Just`), such that the value can be extracted afterwards - just like in an enum:

  enum Maybe<T> {
    Nothing,
    Just(T),
  }

I think it's all right if you're used to the notation. The first two lines are tagged unions and will be recognisable as such if you're familiar with encodings like Scott/Church pairs/lists/numbers. Once you understand the structure, the definition of `bind` becomes obvious, as its two arguments represent the cases "is nothing" and "is just", where in the first case Nothing is returned, and in the second case the function is applied to the value inside the Just.

I think that writing such code, if only for educational purposes, can be really helpful in actually understanding how the state "flows" during the monadic bind/return. Typical monad instantiations of Maybe do not give such deep insight (at least to me).

> Just because you can do a thing doesn’t mean you should.

Of course you should, where would be the fun in that?

They give a nice introduction to encoding state as pure functions. In fact, there are many more purely functional encodings for all kinds of data like trees, integers, sum/product types, images, monads, ...

The encodings can be a bit confusing, but really elegant and tiny at the same time. Take for example a functional implementation of the Maybe monad in javascript:

  Nothing = nothing => just => nothing
  Just = v => nothing => just => just(v)
  
  pure = Just
  bind = mx => f => mx(mx)(f)
  
  evalMaybe = maybe => maybe("Nothing")(v => "Just " + v)
  console.log(evalMaybe(bind(Nothing)(n => pure(n + 1)))) // Nothing
  console.log(evalMaybe(bind(Just(42))(n => pure(n + 1)))) // Just 43

For context since it's not mentioned on the website: This is a project by n-o-d-e[1], they make blog posts and videos about diy tech/mods. This specific project is described in [2].

[1]: https://n-o-d-e.net/

[2]: https://n-o-d-e.net/makeityourself.html

Oddly enough, I've actually researched this topic (and the related "earthing") a lot. It's interesting because there's a surprising amount of research that seems to find positive effects. These results are reinforced by some popular "science" news (sometimes with a remarkable resemblance to pure esotericism).

However, if you dig deeper, you'll find a lot of flaws in these studies. Either suspicious financial conflicts of interest, very small sample groups, confident conclusions despite large error bars, neglect of other influences (such as being more active and outdoors while "earthing"), or just different results between similar studies.

Most studies without obvious flaws or misleading interpretations conclude that much more testing is needed before any useful statement can be made about the effectiveness of grounding/earthing.

I have something similar but for lambda terms with huge normal forms, I always wake up exhausted when this happens

Okay, you've definitely nerd-sniped me here. Actually producing my initial reductions is not as trivial as I thought. Still, I came up with a solution that works for n>2:

  d = λλλλ(3 2 (1 0)) # common
  d' = λλλλλ(4 3 2 (1 0)) # common
  weird = λλλλλ(4 (d (3 2)) 1 0)

Here I use de Bruijn indices instead of named variables and write Church numerals as <n>.

Then,

  (<n-3> weird d' b) ~> λ^{n+1}(n (n-1 (n-2 ... (1 0)..)))

I could explain it in detail if anyone's interested. There should be some more elegant solutions though, so give it a try!

Ah yes, you're right. I messed up the associativity in the reductions.

  (2 b) ~> λhgfx.(h ((g f) x))
  (3 b) ~> λihgfx.(i (((h g) f) x))
  ...

It still does what most interpretations would consider the "nth composition combinator":

  (1 b f g) x = f (g x)
  (2 b f g) x y = f (g x y)
  (3 b f g) x y z = f (g x y z)
  ...

Fun fact: The nth composition combinator can be created by applying the b combinator to the nth Church numeral:

  (1 b) ~> λgfx.(g (f x))
  (2 b) ~> λhgfx.(h (g (f x)))
  (3 b) ~> λihgfx.(i (h (g (f x))))
  ...

Furthermore:

  (X (Y b)) = (X*Y b)

I use these in my bruijn programming language in the form of infix/prefix operators. [1]

[1] https://bruijn.marvinborner.de/std/Combinator.bruijn.html#b

000100011100110100001110011010

Yes, I realize that. However, the alternative using a variadic fixed point combinator looks slightly cleaner and would (optimally) reduce to the same term. For example, using a list-based vfix:

    even' _ odd n = if n == 0 then True else (odd (n - 1)))
    odd' even _ n = if n == 0 then False else (even (n - 1))
    even = head $ vfix [even', odd']
    odd = tail $ vfix [even', odd']

Here, the functions don't need to be passed explicitly to the "recursive" calls. I prefer this a lot, it makes my lambda functions much more readable.

In lambda calculus, you could use a variadic fixed point combinator to solve such recurrence relations elegantly

I wonder what the optimal strategy is, optimize for speed with more fragmentation and fewer operations or for less fragmentation but more operations and time. For 1kb, optimizing for no fragmentation I can't seem to get below ~80.

Thanks for the extensive comment, I agree with you!

However, the project should be viewed from a programmer's perspective, not from a mathematician's. In my opinion the encoding fits the task of approximating specific real and complex numbers good enough, while still being minimal and easy to understand.

For me it doesn't matter that one could encode functions that are not real or paradoxical, not permitting this was never the intention. I improved the wording in the article a bit to make this more obvious.

I do like your idea with the integer pair though, I may try that out in the future :)

It was an introductory talk so you probably didn't miss anything big. Luckily the talk was recorded, so you can re-watch it :)

https://media.ccc.de/v/gpn22-262-programmieren-mit-dem-puren...

(ignore the forgotten night shift)

> With the correct encoding, it's just a mechanical limit

This also applies to small numbers and small mechanical limits. Of course, here the small limits come with the nice side effect of efficiency :)

In general I think you're right. With the correct encoding, it's just a mechanical limit.

It just depends on the specific encoding you use. GMP, I believe, is only limited by the physical memory size. Python's implementation is also limited by the encoding (not sure how it works concretely, but it doesn't seem to be a memory overflow):

  x = 1
  while True:
      x <<= x
  > OverflowError: too many digits in integer

Yes, this is mostly a leftover from initial versions that used a natural number as denominator. It doesn't seem to make a noticeable difference in performance though, since increments are a very basic operation.

I think leaving this in the article makes the non-zero denominator more explicit. It also allows easier adoption to other numeral systems :)

I didn't want to imply that this can't be the case for typical encodings. However, it's rarely the default and is sometimes handled differently than normal numbers (e.g. Haskell's Integer vs Int). Compare this to lambda calculus, where restricting the size of numbers would be the difficult task.

This looks great! Bruijn actually has something similar in its standard library [1] but without your `partition`, so it's much less efficient.

[1]: https://bruijn.marvinborner.de/std/List_Church.bruijn.html#s...

It seems like the prompt is

"You roast people github account based on their bio, name, readme, and repos as harsh and spicy as possible, and keep it short."

https://github.com/codenoid/github-roast/blob/main/src/route...

I believe that if you could also move and link files, you could actually simulate lambda calculus with a similar technique. I imagine something like this would work, where applications are described by shared prefix in same directory depth and order of application is encoded in lexicographical name order:

λx.x:

  $ tree .
  .
  └── x
      └── a -> ../x/

λsz.(s (s (s z))):

  $ tree .
  .
  └── s
      └── z
          ├── a -> ../../s/
          ├── b -> ../../s/
          ├── ca -> ../../s/
          └── cb -> ../z/

Yes, good idea. Maybe I'll add it as an additional method of application. The motivation here was not to find an efficient way to construct terms, but as a fun interpretation of infinite craft. A much simpler solution would obviously be to type the term directly :D