// Get Polylux from the official package repository #import "@preview/polylux:0.4.0": * #set page(paper: "presentation-16-9") #set text(size: 20pt, font: "Cascadia Code") #enable-handout-mode(json(bytes(sys.inputs.at("HANDOUT", default:"false")))) #slide[ #set page(fill:rgb(245,169,184)) #set text(fill: white, size:35pt) #set align(horizon+center) = (。ι‿ι。) Church-encoding text into iotas ] #let clam = [#text(fill: rgb(60,150,180), $#sym.lambda$)] #let cdot = [#text(fill: rgb(60,150,180), $.$)] #let la(a, b) = [#clam #a #cdot #{h(0.5em)} #b] #let S = text(fill: rgb(255, 41, 155), $#math.op("S")$) #let K = text(fill:green,$#math.op("K")$) #let I = text(fill:rgb(145,145,145),$#math.op("I")$) #let zero = text(fill:rgb(145,145,145),$#math.op("zero")$) #let succ = text(fill:purple,$#math.op("succ")$) #let nil = text(fill:red,$#math.op("nil")$) #let cons = text(fill:orange,$#math.op("cons")$) #let iota = text(fill: purple, $#sym.iota$) #let nats = text(fill: red, $ℕ$) #let char(c) = text(fill:green, raw("'" + c + "'")) #slide[ #set text(size: 25pt) = The backstory #v(1em) #set text(size: 18pt) // They say that a peculiar QR code was lying on the final slide of our bachelor prep presentation. A promise of a prize, awaiting those about to scan the code. None lingered long enough to pierce the iota-veiled puzzle, but worry not, for the meaning of the runes shall soon reveal itself to those who seek it. #align(center+horizon)[ #grid(columns:(45%, 45%), [ #image("images/final-slide-fbp.png", height: 50%) A mysterious QR code... ], align(bottom+right)[ #show: later #v(3em) ...leading to peculiar runes #image("images/iota-manuscript.png", height: 50%) ] ) ] ] #slide[ #set align(horizon) = The $clam$-calculus #v(1em) 1. Lamdas: instead of $x ↦ ...$ we write $la(x,...)$ #show: later #v(0.15em) 2. Variable references: for example $la(x, x)$ denotes the identity. #show: later #v(0.15em) 3. Function applications: instead of $f(x)$ we write $f x$. ] #slide[ #set text(size: 25pt) = Multi-parameter functions #v(1em) #set text(size: 23pt) Problem: no products $ f &: nats #sym.times nats -> nats \ f &: (a, b) ↦ a + b $ #show: later Solution: currying! $ g &: nats -> nats -> nats \ g &: a ↦ (b ↦ a + b) $ #align(bottom)[ #set text(size: 11pt) Note: the two are equivalent in a sense because something something adjoint functors, don't worry about it. ] ] #slide[ #set text(size: 25pt) = The #S#K#I combinators #v(1em) #set text(size: 35pt) #align(horizon)[$ #I &:= la(x,x) \ #K &:= la(a,la(b, a)) \ #S &:= la(f, la(a, la(c, (f c) (a c)))) $] ] #slide[ #set text(size: 25pt) #grid(columns:(auto, auto), gutter:20pt, [ = The #S#K#I combinators #v(1em) #set text(size: 23pt) #set align(horizon) Any term in the $clam$-calculus can be written using nothing but the #S#K combinators. #show: later For example $#I := #S #K #S$. ],[ #set align(horizon+center) #uncover(2)[ #image("images/ithinkshespartoftheskteam.jpg", height:80%) ] ]) ] #slide[ #set text(size: 25pt) = A combinator to conquer them all #v(1em) #grid(columns:(auto, auto), gutter: 5pt,[ #set text(size: 18pt) Enter _the $iota$-combinator_! $ iota := la(x, x #S #K) = #S (#S #I (#K #S))(#K #K). $ #show:later We can then define the #S#K#I combinators in terms of $iota$: $ #I &= iota iota \ #K &= iota( iota (iota iota)) \ #S &= iota(iota(iota(iota iota))) $ ],[ #align(horizon)[ #uncover(2)[ #image("images/alwayshasbeenallfunctions.jpg") ] ] ]) ] #slide[ #set text(size: 25pt) = Defining $nats$ #v(1em) #set text(size: 20pt) #set align(horizon) - Problem: we normally define $nats$ using $zero$ and $succ$, but we have neither of those things. - Solution: ask the person using the numbers to provide them! ] #slide[ #set text(size: 25pt) = Defining $nats$ #v(1em) #set text(size: 20pt) Example: instead of defining $1 := succ(zero)$, let $ 1 := la(zero, la(succ, succ " " zero)). $ #show:later We can keep going! $ 2 &:= la(zero, la(succ, succ (succ " " zero)) ) \ 3 &:= la(zero, la(succ,succ( succ (succ " " zero)))) \ 4 &:= la(zero, la(succ,succ(succ( succ (succ " " zero)))))\ dots.v " " & $ ] #slide[ #set text(size: 25pt) = Working with $nats$ #v(1em) #set text(size: 18pt) How do we define addition? 1. The function takes two arguments: $la(a, la(b, ...))$ #show:later 2. The result is also a natural: $la(a, la(b, la(zero, la(succ, ...))))$ // #show:later // 3. The result likely involves $a$: $la(a, la(b, la(zero, la(succ, a " " ? " " ?))))$ #show:later 3. Idea — return $a$, but with its concept of "$zero$" defined as the natural given by $b$: $la(a, la(b, la(zero, la(succ, a " " (b " " zero " " succ) " " succ))))$ $ a + b := la(zero, la(succ, a " " (b " " zero " " succ) " " succ)). $ ] #slide[ #set text(size: 30pt) = Ordered lists #v(1em) #set text(size: 20pt) #align(horizon)[ Ordered lists are surprisingly similar to $nats$. We need: - The empty list (call it $nil$) - A way to go from $a_1, a_2, ..., a_n$ to $x, a_1, a_2, ..., a_n$ (call it $cons$) #show:later Example: We can write $[1, 2, 3]$ as $ la(nil, la(cons, cons " " 1 " " (cons " " 2 " " (cons " " 3 " " nil)))) $ ] #align(bottom)[ #set text(size: 11pt) #uncover(2)[ Note: the naturals are essentially just ordered lists of the unit type, but don't worry about that. ] ] ] #slide[ #grid(columns:(auto, auto), gutter: 10pt, [ #set text(size: 23pt) #v(1em) = The general principle #v(1em) #set text(size: 25pt) #align(horizon)[ - We can encode any inductively defined structure into the $clam$-calculus this way - Named after the logician *Alonzo Church* ] ], image("images/alonzo-church.jpg", height:100%) ) ] #slide[ #set text(size: 30pt) = Encoding text as iotas #v(1em) #set text(size: 25pt) #align(horizon)[ - Strings of text are nothing but ordered lists of characters. - Characters can be represented as naturals (indices inside some alphabet) ] ] #slide[ #set text(size: 30pt) = Encoding text as iotas #v(1em) #set text(size: 25pt) #align(horizon)[ 1. Take the input string, and church-encode it: $ #text(fill:green,```"meow"```) -> #image("images/un-executed-church-encoding.png",height:3em) $ #show:later 2. Normalize (evaluate) the output: #set text(size: 15pt) ```λλ1(λλ1(1(1(1(1(1(1(1(1(1(1(1 0))))))))))))(1(λλ1(1(1(1 0))))(1(λλ1(1(1(1(1(1(1(1(1(1(1(1(1(1 0))))))))))))))(1(λλ1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1(1 0)))))))))))))))))))))) 0)))``` // #set text(size: 10pt) // Without expanding the naturals, the above is essentially // $ la(nil,la(cons,cons " " #char("m") " " (cons " " #char("e") " " (cons " " #char("o") " " (cons " " #char("w") " " nil))))) $ ] ] #slide[ #set text(size: 30pt) = Encoding text as iotas #v(1em) #set text(size: 25pt) #align(horizon)[ 3. Convert to #S#K combinators #set text(size: 15pt) ```S(S(KS)(S(KK)(SI(K(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(KI)))))))))))))))))(S(S(KS)(S(KK)(SI(K(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(KI)))))))))(S(S(KS)(S(KK)(SI(K(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(KI)))))))))))))))))))(S(S(KS)(S(KK)(SI(K(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(S(S(KS)(S(KK)I))(KI)))))))))))))))))))))))))))(KI))))``` ] ] #slide[ #set text(size: 20pt) = The final result #set text(size: 9pt) #align(horizon)[ ```ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ι(ι(ι(ιι)))(ιι)(ι(ι(ιι))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ιι))(ιι))))))))))))))))))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ι(ι(ι(ιι)))(ιι)(ι(ι(ιι))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ιι))(ιι))))))))))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ι(ι(ι(ιι)))(ιι)(ι(ι(ιι))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ιι))(ιι))))))))))))))))))))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ι(ι(ι(ιι)))(ιι)(ι(ι(ιι))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ι(ιι)))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ι(ιι)))))(ι(ι(ι(ιι)))(ι(ι(ιι))(ι(ι(ιι))))(ιι)))(ι(ι(ιι))(ιι))))))))))))))))))))))))))))(ι(ι(ιι))(ιι)))))``` ] ] #slide[ #set page(fill:rgb(245,169,184)) #set text(fill: white) #align(center+horizon)[ #set text(size: 35pt) = But like, isn't this kinda useless ] #show: later #align(center+bottom)[ ...well yeah, the final result kinda is ;-;\ ...but the individual components aren't! ] ] #slide[ #align(horizon)[ #grid(columns:(auto, auto), gutter: 5pt,[ #set text(size: 20pt) = The silver lining #v(1em) #set text(size: 18pt) #align(horizon)[ - The $clam$-calculus itself is extremely important! - Many functional programming languages (Haskell, Lean, etc) have it at their very core! ] ],align(bottom+right)[ // #show: later #image("images/fpmentioned.jpg", height: 100%) ] ) ] ] #slide[ #set page(margin:5pt) #align(center+horizon)[ #set text(size: 18pt) #grid(columns:(35%,35%), gutter:5pt, [ #set align(top) #image("images/slides-qrcode.png", height:50%) Slide repository ], [ #set align(top) #image("images/challenge-qrcode.png", height:50%) The riddle from my team's previous presentation ] ) #set text(size: 35pt) ✨ Thanks You! ✨ ] ] #slide[ #show:later ]