okay so these are slides. if you have a javascript enabled, you should be able to click on one of the little -symbols in order to view like one slide. and then press a and d keys to move back and forward through them. (and press escape to like exit slide mode.) (also also press t to toggle display of current time)
lambda calculus beep boop
recursion: http://llama-the-ultimate.org/slides/flatmap2018
we: @einarwh, @JonasWinje
hi hello
blah
this is mostly about syntax
traditional syntax
Exp u ::= | x | variable |
λx.u | abstraction | |
u1 u2 | application |
replace references to parameter with argument
(λa.λb.λc.c a b) foo bar quux
(λb.λc.c foo b) bar quux
(λc.c foo bar) quux
quux foo bar
some lambdas
0 is λf.λx.x
1 is λf.λx.f x
2 is λf.λx.f (f x)
3 is λf.λx.f (f (f x))
5 is λf.λx.f (f (f (f (f x))))
and so on
some lambdas
+ is λa.λb.λf.λx.a f (b f x)
(f applied a times to f applied b times to x)
* is λa.λb.λf.λx.a (b f) x
(f applied b times a times to x)
can try
2 is λf.λx.f (f x)
3 is λf.λx.f (f (f x))
+ is λa.λb.λf.λx.a f (b f x)
* is λa.λb.λf.λx.a (b f) x
can try
2 is λf.λx.f (f x)
3 is λf.λx.f (f (f x))
+ is λa.λb.λf.λx.a f (b f x)
* is λa.λb.λf.λx.a (b f) x
2 + 3 is (λa.λb.λf.λx.a f (b f x)) (λf.λx.f (f x)) (λf.λx.f (f (f x)))
can try
2 is λf.λx.f (f x)
3 is λf.λx.f (f (f x))
+ is λa.λb.λf.λx.a f (b f x)
* is λa.λb.λf.λx.a (b f) x
2 * 3 is (λa.λb.λf.λx.a (b f) x) (λf.λx.f (f x)) (λf.λx.f (f (f x)))
okay
is traditional
possibly shoutability concerns
variables can be named almost anything
is the untyped lambda calculus sound?
has greek letters in it (hci?)
parentheses
variable capture thing
variable capture thing
λy.(λx.λy.x) y
variable capture thing
λy.(λx.λy.x) y
λy.λy.y
oh no
variable capture thing
λy.(λx.λy.x) y
rename inner y before reducing
λy.(λx.λy2.x) y
λy.λy2.y
de bruijn index
Exp u ::= | n | variable |
λu | abstraction | |
u1 u2 | application |
λz. (λy. y (λx. x)) (λx. z x)
variable capture thing
λy.(λx.λy.x) y
λ(λλ2) 1
variable capture thing
λ(λλ2) 1
λλ2
some lambdas
0 is λλ1
1 is λλ2 1
2 is λλ2 (2 1)
3 is λλ2 (2 (2 1))
5 is λλ2 (2 (2 (2 (2 1))))
and so on
some lambdas
+ is λλλλ4 2 (3 2 1)
(um)
* is λλλλ4 (3 2) 1
(uh)
2 + 3
(λλλλ4 2 (3 2 1)) (λλ2 (2 1)) (λλ2 (2 (2 1)))
(λλλ(λλ2 (2 1)) 2 (3 2 1)) (λλ2 (2 (2 1)))
λλ(λλ2 (2 1)) 2 ((λλ2 (2 (2 1))) 2 1)
λλ(λ3 (3 1)) ((λλ2 (2 (2 1))) 2 1)
λλ2 (2 ((λλ2 (2 (2 1))) 2 1))
λλ2 (2 ((λ3 (3 (3 1))) 1))
λλ2 (2 (2 (2 (2 1))))
2 * 3
(λλλλ4 (3 2) 1) (λλ2 (2 1)) (λλ2 (2 (2 1)))
(λλλ(λλ2 (2 1)) (3 2) 1) (λλ2 (2 (2 1)))
λλ(λλ2 (2 1)) ((λλ2 (2 (2 1))) 2) 1
λλ(λ(λλ2 (2 (2 1))) 3 ((λλ2 (2 (2 1))) 3 1)) 1
λλ(λλ2 (2 (2 1))) 2 ((λλ2 (2 (2 1))) 2 1)
λλ(λ3 (3 (3 1))) ((λλ2 (2 (2 1))) 2 1)
λλ2 (2 (2 ((λλ2 (2 (2 1))) 2 1)))
λλ2 (2 (2 ((λ3 (3 (3 1))) 1)))
λλ2 (2 (2 (2 (2 (2 1)))))
anyway
arithmetic instead of variable capture
subtract 1 from free variables in the function
number of parameter-variable in function increases with depth in syntax tree
add depth to free variables in argument when replacing
fewer possible variable names
still uses greek letters
is the untyped lambda calculus sound??
also still parentheses
maths
beep boop
Exp u ::= | boop b | variable |
beep u | abstraction | |
pling u1 u2 | application |
Boops b ::= | bap | bap |
boop b | boop |
so the identity function is beep boop bap
nice
some beep boops
0 is beep beep boop bap
1 is beep beep pling boop boop bap boop bap
2 is beep beep pling boop boop bap pling boop boop bap boop bap
3 is beep beep pling boop boop bap pling boop boop bap pling boop boop bap boop bap
5 is beep beep pling boop boop bap pling boop boop bap pling boop boop bap pling boop boop bap pling boop boop bap boop bap
and so on
some beep boops
+ is beep beep beep beep pling pling boop boop boop boop bap boop boop bap pling pling boop boop boop bap boop boop bap boop bap
* is beep beep beep beep pling pling boop boop boop boop bap pling boop boop boop bap boop boop bap boop bap
2 + 3
pling pling beep beep beep beep pling pling boop boop boop boop bap boop boop bap pling pling boop boop boop bap boop boop bap boop bap beep beep pling boop boop bap pling boop boop bap boop bap beep beep pling boop boop bap pling boop boop bap pling boop boop bap boop bap
can try
good stuff
okay
there's another evaluator
and another one
2 + 3
pling pling beep beep beep beep pling pling boop boop boop boop bap boop boop bap pling pling boop boop boop bap boop boop bap boop bap beep beep pling boop boop bap pling boop boop bap boop bap beep beep pling boop boop bap pling boop boop bap pling boop boop bap boop bap
2 * 3
pling pling beep beep beep beep pling pling boop boop boop boop bap pling boop boop boop bap boop boop bap boop bap beep beep pling boop boop bap pling boop boop bap boop bap beep beep pling boop boop bap pling boop boop bap pling boop boop bap boop bap
so
no parentheses
a small set of not very difficult words
solves hci issues by being intuitive for both humans and computers
“making illegal states unrepresentable”
we
accept beep, boop, pling
or accept boop, bap
or are done
“making illegal states unrepresentable”
easy to keep track of how many expressions we need
starts at 1
increases by 1 when pling
decreases by 1 when boop-bap
neat
the beep boop software suite, enterprise addons
is the untyped lambda calculus sound???
does the untyped lambda calculus make sound?????
does the untyped lambda calculus make sound?????
replace the keyboard with a keyboard
more soundness
also voice recognition
syntax colouring
fish!
plug-in architecture
function supersaw(freq, vol, sawNumber, detune) { var g = audioContext.createGain(); g.gain.setValueAtTime(0, audioContext.currentTime); for (var i = 0; i < sawNumber; i++) { var saw = audioContext.createOscillator(); saw.type = 'sawtooth'; saw.frequency.setValueAtTime(freq, audioContext.currentTime); saw.detune.value = -detune + i * 2 * (detune / (sawNumber - 1)); saw.start(); saw.connect(g); } var dur = 0; for (var i = 0; i < vol.length; i++) { dur = dur + vol[i].time; } dur = dur * 0.5; g.connect(audioContext.destination); return note(dur, [{ dial: g.gain, vts: vol }]); } const sawVol = [ { val: 0.13, time: 0.1 }, { val: 0.1, time: 0.2 }, { val: 0.1, time: 0.5 }, { val: 0, time: 0.3 }]; function saw(freq) { return supersaw(freq, vol, 7, 10); } notes = [saw(440), saw(493.88), saw(523.25), saw(587.33), saw(800), saw(250)];
okay bye
notes = makeNotes(x =>[{ val: x * 1.2, time: 0.7 }, { val: x, time: 0.3 }], vol,[400, 460, 515, 550, 800, 250]);