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)

#0

#1

hi hello


#2

blah

this is mostly about syntax


#3

traditional syntax


#4

Exp u ::=xvariable
λx.uabstraction
u1 u2application


#5

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


#6

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


#7

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)


#8

can try

evaluator

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


#9

can try

evaluator

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)))


#10

can try

evaluator

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)))


#11

okay


#12

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


#13

variable capture thing

λy.(λx.λy.x) y


#14

variable capture thing

λy.(λx.λy.x) y

λy.λy.y

oh no


#15

variable capture thing

λy.(λx.λy.x) y

rename inner y before reducing

λy.(λx.λy2.x) y

λy.λy2.y


#16

de bruijn index


#17

Exp u ::=nvariable
λuabstraction
u1 u2application


#18

λz. (λy. y (λx. x)) (λx. z x)


#19

variable capture thing

λy.(λx.λy.x) y

λ(λλ2) 1


#20

variable capture thing

λ(λλ2) 1

λλ2


#21

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


#22

some lambdas

+ is λλλλ4 2 (3 2 1)

(um)

* is λλλλ4 (3 2) 1

(uh)


#23

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))))


#24

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)))))


#25

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


#26

fewer possible variable names

still uses greek letters

is the untyped lambda calculus sound??

also still parentheses

maths


#27

beep boop


#28

Exp u ::=boop bvariable
beep uabstraction
pling u1 u2application

Boops b ::=bapbap
boop bboop


#29

so the identity function is beep boop bap

nice


#30

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


#31

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


#32

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


#33

#34

good stuff


#35

okay

there's another evaluator


#36

#37

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


#38

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


#39

so


#40

no parentheses

a small set of not very difficult words

solves hci issues by being intuitive for both humans and computers


#41

“making illegal states unrepresentable”

we

accept beep, boop, pling

or accept boop, bap

or are done


#42

“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


#43

neat


#44

the beep boop software suite, enterprise addons


#45

is the untyped lambda calculus sound???


#46

does the untyped lambda calculus make sound?????


#47

does the untyped lambda calculus make sound?????

noisy editor


#48

replace the keyboard with a keyboard


#49

more soundness

noisy evaluator


#50

also voice recognition


#51

syntax colouring

graphical evaluator


#52

#53

plug-in architecture

evaluator

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)];


#54

(supersaw stolen from @mollerse. code.)


#55

be glad for the song has no ending

evaluator


#56

okay bye

notes = makeNotes(x =>[{ val: x * 1.2, time: 0.7 }, { val: x, time: 0.3 }], vol,[400, 460, 515, 550, 800, 250]);


#57