commit 1adcb66891f342483c3eb59b34190af8cfd9a22b Author: prescientmoon <git@moonythm.dev> Date: Tue Apr 29 17:10:58 2025 +0200 Start working on the slides diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..31da9cd --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +iotas.pdf +result diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..e62d37b --- /dev/null +++ b/flake.lock @@ -0,0 +1,82 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1744932701, + "narHash": "sha256-fusHbZCyv126cyArUwwKrLdCkgVAIaa/fQJYFlCEqiU=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "b024ced1aac25639f8ca8fdfc2f8c4fbd66c48ef", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs", + "typix": "typix" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "typix": { + "inputs": { + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1745311617, + "narHash": "sha256-rSwSFTy7E+/i+V2IB6GT4eP07r0XPoKlq/GbNYhakkw=", + "owner": "loqusion", + "repo": "typix", + "rev": "bc85fe6c66247893e8ff3e5d15166276caaf26eb", + "type": "github" + }, + "original": { + "owner": "loqusion", + "repo": "typix", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..6606d15 --- /dev/null +++ b/flake.nix @@ -0,0 +1,66 @@ +{ + inputs = { + nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; + flake-utils.url = "github:numtide/flake-utils"; + + typix = { + url = "github:loqusion/typix"; + inputs.nixpkgs.follows = "nixpkgs"; + }; + }; + + outputs = + inputs: + inputs.flake-utils.lib.eachSystem (with inputs.flake-utils.lib.system; [ x86_64-linux ]) ( + system: + let + pkgs = inputs.nixpkgs.legacyPackages.${system}; + typixLib = inputs.typix.lib.${system}; + lib = pkgs.lib; + + src = lib.fileset.toSource { + root = ./.; + fileset = lib.fileset.unions [ + ./images + ./iotas.typ + ]; + }; + + commonArgs = handout: { + typstSource = "iotas.typ"; + fontPaths = [ "${pkgs.cascadia-code}/share/fonts/truetype" ]; + virtualPaths = [ ]; + unstable_typstPackages = [ + { + name = "polylux"; + version = "0.4.0"; + hash = "sha256-4owP2KiyaaASS1YZ0Hs58k6UEVAqsRR3YdGF26ikosk="; + } + ]; + + typstOpts.format = "pdf"; + typstOpts.input = "HANDOUT=${if handout then "true" else "false"}"; + }; + + buildPresentation = handout: typixLib.buildTypstProject ((commonArgs handout) // { inherit src; }); + + presentation = pkgs.linkFarm "coles-presentation" [ + { + path = buildPresentation false; + name = "slides.pdf"; + } + { + path = buildPresentation true; + name = "handout.pdf"; + } + ]; + in + { + devShell = pkgs.mkShell { + nativeBuildInputs = [ pkgs.typst ]; + }; + + packages.default = presentation; + } + ); +} diff --git a/images/alonzo-church.jpg b/images/alonzo-church.jpg new file mode 100644 index 0000000..304710d Binary files /dev/null and b/images/alonzo-church.jpg differ diff --git a/images/darkcave.jpg b/images/darkcave.jpg new file mode 100644 index 0000000..d388d46 Binary files /dev/null and b/images/darkcave.jpg differ diff --git a/images/executed-church-encoding.png b/images/executed-church-encoding.png new file mode 100644 index 0000000..eab64a7 Binary files /dev/null and b/images/executed-church-encoding.png differ diff --git a/images/final-slide-fbp.png b/images/final-slide-fbp.png new file mode 100644 index 0000000..0304c5d Binary files /dev/null and b/images/final-slide-fbp.png differ diff --git a/images/fpmentioned.jpg b/images/fpmentioned.jpg new file mode 100644 index 0000000..5762f98 Binary files /dev/null and b/images/fpmentioned.jpg differ diff --git a/images/iota-manuscript.png b/images/iota-manuscript.png new file mode 100644 index 0000000..3491280 Binary files /dev/null and b/images/iota-manuscript.png differ diff --git a/images/ithinkshespartoftheskteam.jpg b/images/ithinkshespartoftheskteam.jpg new file mode 100644 index 0000000..c9cf71e Binary files /dev/null and b/images/ithinkshespartoftheskteam.jpg differ diff --git a/images/un-executed-church-encoding.png b/images/un-executed-church-encoding.png new file mode 100644 index 0000000..0cff05f Binary files /dev/null and b/images/un-executed-church-encoding.png differ diff --git a/iotas.typ b/iotas.typ new file mode 100644 index 0000000..4cf238d --- /dev/null +++ b/iotas.typ @@ -0,0 +1,324 @@ +// 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[ + = 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) + = The #S#K#I combinators + #v(1em) + #set text(size: 23pt) + + - Any term in the $clam$-calculus can be written using nothing but the #S#K combinators. #later[For example $#I := #S #K #S$. + + #align(horizon+center)[ + #image("images/ithinkshespartoftheskteam.jpg", width:40%) + ] +] +] + +#slide[ + #set text(size: 25pt) + = A combinator to conquer them all + #v(1em) + #set text(size: 20pt) + + 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))) + $ +] + +#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) + 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[ + #align(center+horizon)[ + #set text(size: 35pt) + ✨ Thanks You! ✨ + ] +] + +#slide[ #show:later ]