Show HN: A lambda expression visualizer for the web (opens in new tab)

(brycec.github.com)

43 pointsnotb13y ago11 comments

11 comments

notbOP13y ago

The source is kinda crude at this point, but I hope to eventually allow named abstractions as well as direct manipulation of the tree (click n drag). Supporting types might be interesting as well.

Sniffnoy13y ago

The notation is cumbersome, but I like the visualization. I wish eta-reduction were implemented rather than just beta-reduction.

Unfortunately there appear to be some errors. Try entering the following expression:

#(##2 1)

This, if I've understood the notation correctly, means λx.(λy.λz.y)x. Thus, it should reduce to λx.λz.x, or ##2. However, the program instead reduces it to ##1, or λx.λz.z.

So, something's really wrong here.

notbOP13y ago

Agreed, it is unwieldy. However, because of it, eta-reduction is not as important because equivalent terms look the same, and name collisions can't happen. It made it a bit simpler.

And, that is definitely a bug, thanks. I think I could solve it by lazy evaluation (it wouldn't reduce that term) but I think I just need to correctly change vars when they move scope.

Sniffnoy13y ago

Not sure what you mean by "equivalent terms look the same". I'm not clear on how e.g. ##(2 1) and #1 look the same. Going by your remark about name collisions, I must ask if you are thinking of alpha-equivalence? (Which certainly is rendered unnecessary by the notational system.)

And thank you for making/hopefully fixing this!

1 more reply

DanWaterworth13y ago

The text at the bottom says this is simply typed lambda calculus, but surely this is untyped lambda calculus.

notbOP13y ago

Right, thanks! Corrected.

tqs13y ago

I think this would be really great with back and forward controls, i.e. rewind.

j / k navigate · click thread line to collapse

11 comments

notbOP13y ago

The source is kinda crude at this point, but I hope to eventually allow named abstractions as well as direct manipulation of the tree (click n drag). Supporting types might be interesting as well.

Sniffnoy13y ago

The notation is cumbersome, but I like the visualization. I wish eta-reduction were implemented rather than just beta-reduction.

Unfortunately there appear to be some errors. Try entering the following expression:

#(##2 1)

This, if I've understood the notation correctly, means λx.(λy.λz.y)x. Thus, it should reduce to λx.λz.x, or ##2. However, the program instead reduces it to ##1, or λx.λz.z.

So, something's really wrong here.

notbOP13y ago

Agreed, it is unwieldy. However, because of it, eta-reduction is not as important because equivalent terms look the same, and name collisions can't happen. It made it a bit simpler.

And, that is definitely a bug, thanks. I think I could solve it by lazy evaluation (it wouldn't reduce that term) but I think I just need to correctly change vars when they move scope.

Sniffnoy13y ago

And thank you for making/hopefully fixing this!

1 more reply

DanWaterworth13y ago

The text at the bottom says this is simply typed lambda calculus, but surely this is untyped lambda calculus.

notbOP13y ago

Right, thanks! Corrected.

tqs13y ago

I think this would be really great with back and forward controls, i.e. rewind.

j / k navigate · click thread line to collapse