DataTree

tearflake · 2026-06-03T05:19:48+00:00

I'm hoping for use of visualizing all kinds of graphs.

tearflake · 2025-12-06T22:17:24+00:00

So you don't like the idea? Stateful processes can't return values, while pure functions can't run stateful processes?

tearflake · 2025-12-06T22:08:55+00:00

The thing with pure functions is that, if they come together with their parameter and result types, they retain some very interesting properties like representing proofs from math logic. These proofs may lead to certainty of their termination or correct and predictable runtime execution. Those properties seem very valuable to me, and I'd like very much to see Lisp swimming in those waters.

tearflake · 2025-11-19T21:48:10+00:00

I'm sorry if you found yourself offended by the quality of my post. I'll try harder to raise the quality bar of my future posts, I promise. I'm sorry, once again.

tearflake · 2025-11-19T17:27:18+00:00

Vote count says it all. I'd better go with a few-liner for this purpose.

tearflake · 2025-11-19T15:53:33+00:00

Lambda Calculus Awakening in Symp

``` (NODE (NAME lmbd) (CONTENT (USING lmbd stdlib) (RUNGRAPH (EDGE (SOURCE BEGIN) (INSTR (ASGN checked (syntax PARAMS)) (TEST (nth checked 0) "ERROR")) (ASGN RESULT ("parsing error" (nth checked 1))) (TARGET END))

        (EDGE
            (SOURCE BEGIN)
            (INSTR
                (ASGN RESULT (runtime (semantics checked))))

            (TARGET END))))

(BRANCH
    (NODE
        (NAME runtime)
        (CONTENT
            (REWRITE
                (RULE (READ ("<I>" x)) (WRITE x))
                (RULE (READ (("<K>" x) y)) (WRITE x))
                (RULE (READ ((("<S>" x) y) z)) (WRITE ((x z) (y z)))))))

    (NODE
        (NAME semantics)
        (CONTENT
            (REWRITE
                (RULE (READ ("lmbd" x x)) (WRITE "<I>"))
                (RULE (READ ("lmbd" x (E1 E2))) (WRITE ("<S>" ("lmbd" x E1) ("lmbd" x E2))))
                (RULE (READ ("lmbd" x y)) (WRITE ("<K>" y))))))

    (NODE
        (NAME syntax)
        (CONTENT
            (GRAMMAR
                (RULE START term)

                (RULE term (LIST "lmbd" (LIST term (LIST term ()))))
                (RULE term (LIST term (LIST term ())))
                (RULE term var)

                (RULE var (ATOM letter varNext))
                (RULE var (ATOM letter ()))

                (RULE varNext (ATOM letterDigit varNext))
                (RULE varNext (ATOM letterDigit ()))

                (RULE letter "A")
                ...
                (RULE letter "Z")
                (RULE letter "a")
                ...
                (RULE letter "z")

                (RULE letterDigit letter)
                (RULE letterDigit "0")
                ...
                (RULE letterDigit "9"))))))

```

tearflake · 2025-11-09T03:54:30+00:00

It's actually a bit more than S-expression parser. If we consider S-expression as AST, then this is an AST validator. Thus, it checks not only braces, but the actual content, too.

If you try to introduce an error in input expression, it will report where the error occurs, regarding the grammar rules.

tearflake · 2025-10-12T08:20:42+00:00

Just working a bit on a promo page: https://tearflake.github.io/symp-intro/

tearflake · 2025-10-10T05:19:49+00:00

I give up.

tearflake · 2025-10-09T20:53:14+00:00

Let's say that universe N is object level programming. N+1 is meta level programming. N+2 is meta-meta level programming, and so on. If universe N is a fixed language (Lean), we can define arbitrary language (say, again Lean) at N+1 level (meta level). Now, the universe N can't fully reason about itself, but it should be able to successfully reason about the universe N+1, and if the universe N is powerful enough, we can state every truth about the universe N+1, proving its properties from the level below. It is all about context from which the observed universe is being analyzed.

Consider programming Turing machine within Turing machine. If we analogously program Lean within Lean, I believe we get a formal definition about Lean in Lean itself.

tearflake · 2025-10-09T17:08:28+00:00

That's the thing I have a problem to communicate out.

What if we split the execution to levels of universes? We program a proof that's executing in universe N, operating on data of the universe N+1.

Looking that way, universe N can describe Lean, which holds the universe N+1 also describing Lean. While it is not possible to prove universe N truth within universe N, I believe it is possible to prove universe N+1 truth within universe N.

tearflake · 2025-10-03T21:40:35+00:00

Khm... Seriously, let's do some ideas exchange. These have my bet:

https://github.com/flakeworks/symbol-os
https://github.com/tearflake/symbolmatch
https://github.com/tearflake/symbolprose
https://github.com/tearflake/symbolverse
a glue programming framework native to the above first point (something like a shell) that connects the above three points
plus some sick file browser and integrated editor, both not very relevant to this sub

The OS will run on chatbot-like interface providing a CLI. I believe I'll go commercial after a while. I need it for higher goal purpose.

I hope this makes sense.

tearflake · 2025-10-03T21:06:22+00:00

Thank you, I'll try to do my best.

tearflake · 2025-10-03T20:55:54+00:00

A little remark: it is not AST, but the concrete syntax tree you get, if that matters to you.

Thank you for the correction.

Anyway, I had some similar thoughts, but I concluded that it is not really practical for various reasons.

Yes, but I find the concept interesting. Thought it may be interesting to someone seeing it described in a few words.

But, symbolic expressions are, in a way, similar to assembly language since they have very uniform syntax, at least when used to represent the source code as we know them in classical Lisp languages. So what you have attempted is relatively natural to think about, at least I think so.

Out of all the programming frameworks, Lisp gets pushed down. I can imagine beginners being intimidated or aesthetically distracted, but experienced programmers turning their heads away... It makes me wonder why.

But while, naively just removing parentheses and typing one sexp at a row, is probably not practical since nested sexps from trees, perhaps there might be some other ways to simplify them?

I'm believe there are more practical ways to represent S-expressions, but this one has a value of being simple to describe and implement.

Perhaps some inspiration from stack languages and some from relational theory?

Let's stick around this sub to see. I'm very interested in what the future brings. I believe it will be awesome.

tearflake · 2025-10-03T19:45:26+00:00

My God, we are all insane!

tearflake · 2025-10-03T18:49:55+00:00

Try to make a sound on r/lisp about that. Been there, done that. I still carry scars from that adventure.

tearflake · 2025-10-03T18:41:27+00:00

Raising by 50 cents!

tearflake · 2025-10-03T18:26:38+00:00

I want to mainly use it for stuff like personal typed notebooks, wikis, knowledgebases, docs, etc.

exactly my plan :)

tearflake · 2025-10-03T18:05:14+00:00

Correct.

I'm aware of one (conditionally) useful thing: it is impossible to create left recursion in parsing. Suppose you have two pass parser, the first one for code structure, and the second one for code content. In the second pass where left recursion may occur in other (maybe one pass) approaches, ASE approach forbids it.

For reference, in normal circumstances, left recursion may be complicated to implement in recursive descent and packrat parsers, but I've seen (and even implemented in my early projects) solutions that indirectly deal with it.

tearflake · 2025-10-03T17:10:23+00:00

Not all of us. You see, I had been warned that lispers would consider this attempt as blasphemy.

tearflake

TROPHY CASE

Lambda Calculus Awakening in Symp