some graphical algorithm notation

Stream: lean4

[Locria Cyber]

@Jad Ghalayini

[Locria Cyber]

1.jpg 2.jpg 3.jpg

[Locria Cyber]

This is inspired by Koka. When effects are lifted, the language no longer subject to linearity of lambda calculus.

[Locria Cyber]

a -> b -> c is the same as b -> a -> c

[Locria Cyber]

And different effects do not need to be sequenced one after another. The trivial implementation of map in my language allows the compiler to parallelize it.

[Locria Cyber]

In fact, the language is so free about effects that I have to invent causality constraint (similar to atomic order, but as hint for compiler not to parallelize). See Picture 3.

[Locria Cyber]

When I replicate simple UNIX programs in this language, I found myself sometimes forget to add causality constraints (downside).

[Locria Cyber]

The upside is, the compiler knows about causality relationship of your code.

[Locria Cyber]

See lower half of Picture 1. A function that emits two entangled effects (represented as coiled together) cannot be cut in two, while a function with two not-entangled effects can.

[Locria Cyber]

This language is very friendly to refactoring. You can cut any algorithm in any way, and the resulting parts are still valid in this language.

[Henrik Böving]

Is there a particular reason you are sharing this here?

[Locria Cyber]

Because I saw the work @Jad Ghalayini is doing.

[Locria Cyber]

This thread not really belong to #lean4. How do I move it somewhere else?

[Eric Wieser]

I'm not sure whether this really belongs anywhere, but my closest guesses would be, in order of relevance:

• In a private message to Jad Ghalayini
• In #new members
• In #Program verification
• In #Type theory, maybe

[Eric Wieser]

This is how you can move your own message:

image.png

[Henrik Böving]

Moving messages is actually a privilege reserved to people with moderator powers or higher @Eric Wieser at least that button is not here for me.

[Eric Wieser]

Ah you're right, non-moderators can only move their messages within a stream (by editing the title)

[Jad Ghalayini]

@Locria Cyber fascinating; I'd be happy to discuss this further, seens related to my work! Would you mind sending me an e-mail?

[Jad Ghalayini]

Probably not the best place haha