How do the lambdas?

(2017-07-12. Index.)

This post is part of a list: Some lambda-notes
Next thing: What do the lambdas?
Previous thing: Some numbery functions

A readonly editor is readonly. Its content is evaluated when page loads or so. Mostly for adding definitions to toplevel so they can be used later in the post:

id ≜ λx.x 0 ≜ λf.λx.x ω ≜ λx.x x

In the regular editors we can do stuff.

(can do stuff here)

Normal text-editor-stuff should work. Lambdastuff in addition:

ctrl+enter, ctrl+shift+enter and ctrl+r all work on the line the cursor is on. Results are printed on new line(s), after. (And cursor moves to end of result.)


So, normally, if we have written some term that maybe uses some of the toplevel defintions, we do ctrl+r and then either ctrl+enter a few times, or ctrl+shift+enter once. Can try:

(λa.λb.b a) 0 ω 0

Lines with (or := are for definitons). ctrl+enter on a line that goes like <identifier> ≜ <term> adds a definition.

S ≜ λn.λf.λx.f (n f x)

(Most characters can be used in identifiers. Just, not whitespace ones, and not the ones that are used for other stuff: :, \, , λ, ., (, ).)

The terms used in definitions can use the names of defintions that already exist. Like, we can define 2 like this now, as long as we have defined 0 and S first: (ctrl+enter)

2 ≜ S (S 0)

(We can evaluate it to check that the result looks reasonably twoish. Two applications of f is very two-like, so the result should look like λf.λx.f (f x). (ctrl+r, then ctrl+shift+enter))

2

If we wanna get rid of a definition we can do <identifier> ≜ :(, or just <identifier> ≜. We’ll remove ω (it’s scary): (ctrl+enter)

ω ≜ :(

If we try to evaluate the thing we did earler, we won’t get the same result now, since ω will just be treated as some free variable... (ctrl+r, then ctrl+shift+enter)

(λa.λb.b a) 0 ω 0

That’s like more or less it. In posts like this it’s mostly enough to do ctrl+enter on definitions, and ctrl+r and then ctrl+shift+enter on other stuff...

The evaluation of the lambda-things is mostly done with this bit of PureScript-code. The editors are Monaco ones...