diff --git a/astro.config.ts b/astro.config.ts index b5c9750..39d6d3e 100644 --- a/astro.config.ts +++ b/astro.config.ts @@ -8,6 +8,9 @@ import emoji from "remark-emoji"; import remarkMermaid from "astro-diagram/remark-mermaid"; import remarkDescription from "astro-remark-description"; import remarkAdmonitions from "./plugin/remark-admonitions"; +import remarkMath from "remark-math"; + +import rehypeKatex from "rehype-katex"; // https://astro.build/config export default defineConfig({ @@ -18,9 +21,11 @@ export default defineConfig({ remarkPlugins: [ remarkAdmonitions, remarkReadingTime, + remarkMath, remarkMermaid, emoji, [remarkDescription, { name: "excerpt" }], ], + rehypePlugins: [rehypeKatex], }, }); diff --git a/package-lock.json b/package-lock.json index 73670fb..141f0b5 100644 --- a/package-lock.json +++ b/package-lock.json @@ -16,11 +16,14 @@ "astro-imagetools": "^0.9.0", "astro-remark-description": "^1.0.1", "fork-awesome": "^1.2.0", + "katex": "^0.16.8", "lodash-es": "^4.17.21", "mdast-util-to-string": "^4.0.0", "reading-time": "^1.5.0", + "rehype-katex": "^6.0.3", "remark-emoji": "^4.0.0", "remark-github-beta-blockquote-admonitions": "^2.1.0", + "remark-math": "^5.1.1", "remark-parse": "^10.0.2" }, "devDependencies": { @@ -1574,6 +1577,11 @@ "resolved": "https://registry.npmjs.org/@types/json5/-/json5-0.0.30.tgz", "integrity": "sha512-sqm9g7mHlPY/43fcSNrCYfOeX9zkTTK+euO5E6+CVijSMm5tTjkVdwdqRkY3ljjIAf8679vps5jKUoJBCLsMDA==" }, + "node_modules/@types/katex": { + "version": "0.14.0", + "resolved": "https://registry.npmjs.org/@types/katex/-/katex-0.14.0.tgz", + "integrity": "sha512-+2FW2CcT0K3P+JMR8YG846bmDwplKUTsWgT2ENwdQ1UdVfRk3GQrh6Mi4sTopy30gI8Uau5CEqHTDZ6YvWIUPA==" + }, "node_modules/@types/lodash": { "version": "4.14.197", "resolved": "https://registry.npmjs.org/@types/lodash/-/lodash-4.14.197.tgz", @@ -3148,6 +3156,17 @@ "once": "^1.4.0" } }, + "node_modules/entities": { + "version": "4.5.0", + "resolved": "https://registry.npmjs.org/entities/-/entities-4.5.0.tgz", + "integrity": "sha512-V0hjH4dGPh9Ao5p0MoRY6BVqtwCjhz6vI5LT8AJ55H+4g9/4vbHx1I54fS0XuclLhDHArPQCiMjDxjaL8fPxhw==", + "engines": { + "node": ">=0.12" + }, + "funding": { + "url": "https://github.com/fb55/entities?sponsor=1" + } + }, "node_modules/es-module-lexer": { "version": "1.3.0", "resolved": "https://registry.npmjs.org/es-module-lexer/-/es-module-lexer-1.3.0.tgz", @@ -3694,6 +3713,61 @@ "node": ">=4" } }, + "node_modules/hast-util-from-dom": { + "version": "4.2.0", + "resolved": "https://registry.npmjs.org/hast-util-from-dom/-/hast-util-from-dom-4.2.0.tgz", + "integrity": "sha512-t1RJW/OpJbCAJQeKi3Qrj1cAOLA0+av/iPFori112+0X7R3wng+jxLA+kXec8K4szqPRGI8vPxbbpEYvvpwaeQ==", + "dependencies": { + "hastscript": "^7.0.0", + "web-namespaces": "^2.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, + "node_modules/hast-util-from-html": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/hast-util-from-html/-/hast-util-from-html-1.0.2.tgz", + "integrity": "sha512-LhrTA2gfCbLOGJq2u/asp4kwuG0y6NhWTXiPKP+n0qNukKy7hc10whqqCFfyvIA1Q5U5d0sp9HhNim9gglEH4A==", + "dependencies": { + "@types/hast": "^2.0.0", + "hast-util-from-parse5": "^7.0.0", + "parse5": "^7.0.0", + "vfile": "^5.0.0", + "vfile-message": "^3.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, + "node_modules/hast-util-from-html-isomorphic": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/hast-util-from-html-isomorphic/-/hast-util-from-html-isomorphic-1.0.0.tgz", + "integrity": "sha512-Yu480AKeOEN/+l5LA674a+7BmIvtDj24GvOt7MtQWuhzUwlaaRWdEPXAh3Qm5vhuthpAipFb2vTetKXWOjmTvw==", + "dependencies": { + "@types/hast": "^2.0.0", + "hast-util-from-dom": "^4.0.0", + "hast-util-from-html": "^1.0.0", + "unist-util-remove-position": "^4.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, + "node_modules/hast-util-from-html/node_modules/parse5": { + "version": "7.1.2", + "resolved": "https://registry.npmjs.org/parse5/-/parse5-7.1.2.tgz", + "integrity": "sha512-Czj1WaSVpaoj0wbhMzLmWD69anp2WH7FXMB9n1Sy8/ZFF9jolSQVMu1Ij5WIyGmcBmhk7EOndpO4mIpihVqAXw==", + "dependencies": { + "entities": "^4.4.0" + }, + "funding": { + "url": "https://github.com/inikulin/parse5?sponsor=1" + } + }, "node_modules/hast-util-from-parse5": { "version": "7.1.2", "resolved": "https://registry.npmjs.org/hast-util-from-parse5/-/hast-util-from-parse5-7.1.2.tgz", @@ -3712,6 +3786,19 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/hast-util-is-element": { + "version": "2.1.3", + "resolved": "https://registry.npmjs.org/hast-util-is-element/-/hast-util-is-element-2.1.3.tgz", + "integrity": "sha512-O1bKah6mhgEq2WtVMk+Ta5K7pPMqsBBlmzysLdcwKVrqzZQ0CHqUPiIVspNhAG1rvxpvJjtGee17XfauZYKqVA==", + "dependencies": { + "@types/hast": "^2.0.0", + "@types/unist": "^2.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/hast-util-parse-selector": { "version": "3.1.1", "resolved": "https://registry.npmjs.org/hast-util-parse-selector/-/hast-util-parse-selector-3.1.1.tgz", @@ -3825,6 +3912,21 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/hast-util-to-text": { + "version": "3.1.2", + "resolved": "https://registry.npmjs.org/hast-util-to-text/-/hast-util-to-text-3.1.2.tgz", + "integrity": "sha512-tcllLfp23dJJ+ju5wCCZHVpzsQQ43+moJbqVX3jNWPB7z/KFC4FyZD6R7y94cHL6MQ33YtMZL8Z0aIXXI4XFTw==", + "dependencies": { + "@types/hast": "^2.0.0", + "@types/unist": "^2.0.0", + "hast-util-is-element": "^2.0.0", + "unist-util-find-after": "^4.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/hast-util-whitespace": { "version": "2.0.1", "resolved": "https://registry.npmjs.org/hast-util-whitespace/-/hast-util-whitespace-2.0.1.tgz", @@ -4382,6 +4484,29 @@ "resolved": "https://registry.npmjs.org/jsonc-parser/-/jsonc-parser-3.2.0.tgz", "integrity": "sha512-gfFQZrcTc8CnKXp6Y4/CBT3fTc0OVuDofpre4aEeEpSBPV5X5v4+Vmx+8snU7RLPrNHPKSgLxGo9YuQzz20o+w==" }, + "node_modules/katex": { + "version": "0.16.8", + "resolved": "https://registry.npmjs.org/katex/-/katex-0.16.8.tgz", + "integrity": "sha512-ftuDnJbcbOckGY11OO+zg3OofESlbR5DRl2cmN8HeWeeFIV7wTXvAOx8kEjZjobhA+9wh2fbKeO6cdcA9Mnovg==", + "funding": [ + "https://opencollective.com/katex", + "https://github.com/sponsors/katex" + ], + "dependencies": { + "commander": "^8.3.0" + }, + "bin": { + "katex": "cli.js" + } + }, + "node_modules/katex/node_modules/commander": { + "version": "8.3.0", + "resolved": "https://registry.npmjs.org/commander/-/commander-8.3.0.tgz", + "integrity": "sha512-OkTL9umf+He2DZkUq8f8J9of7yL6RJKI24dVITBmNfZBmri9zYZQrKkuXiKhyfPSu8tUhnVBB1iKXevvnlR4Ww==", + "engines": { + "node": ">= 12" + } + }, "node_modules/khroma": { "version": "2.0.0", "resolved": "https://registry.npmjs.org/khroma/-/khroma-2.0.0.tgz", @@ -4791,6 +4916,20 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/mdast-util-math": { + "version": "2.0.2", + "resolved": "https://registry.npmjs.org/mdast-util-math/-/mdast-util-math-2.0.2.tgz", + "integrity": "sha512-8gmkKVp9v6+Tgjtq6SYx9kGPpTf6FVYRa53/DLh479aldR9AyP48qeVOgNZ5X7QUK7nOy4yw7vg6mbiGcs9jWQ==", + "dependencies": { + "@types/mdast": "^3.0.0", + "longest-streak": "^3.0.0", + "mdast-util-to-markdown": "^1.3.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/mdast-util-mdx": { "version": "2.0.1", "resolved": "https://registry.npmjs.org/mdast-util-mdx/-/mdast-util-mdx-2.0.1.tgz", @@ -5205,6 +5344,29 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/micromark-extension-math": { + "version": "2.1.2", + "resolved": "https://registry.npmjs.org/micromark-extension-math/-/micromark-extension-math-2.1.2.tgz", + "integrity": "sha512-es0CcOV89VNS9wFmyn+wyFTKweXGW4CEvdaAca6SWRWPyYCbBisnjaHLjWO4Nszuiud84jCpkHsqAJoa768Pvg==", + "dependencies": { + "@types/katex": "^0.16.0", + "katex": "^0.16.0", + "micromark-factory-space": "^1.0.0", + "micromark-util-character": "^1.0.0", + "micromark-util-symbol": "^1.0.0", + "micromark-util-types": "^1.0.0", + "uvu": "^0.5.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, + "node_modules/micromark-extension-math/node_modules/@types/katex": { + "version": "0.16.2", + "resolved": "https://registry.npmjs.org/@types/katex/-/katex-0.16.2.tgz", + "integrity": "sha512-dHsSjSlU/EWEEbeNADr3FtZZOAXPkFPUO457QCnoNqcZQXNqNEu/svQd0Nritvd3wNff4vvC/f4e6xgX3Llt8A==" + }, "node_modules/micromark-extension-mdx-expression": { "version": "1.0.8", "resolved": "https://registry.npmjs.org/micromark-extension-mdx-expression/-/micromark-extension-mdx-expression-1.0.8.tgz", @@ -6738,6 +6900,37 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/rehype-katex": { + "version": "6.0.3", + "resolved": "https://registry.npmjs.org/rehype-katex/-/rehype-katex-6.0.3.tgz", + "integrity": "sha512-ByZlRwRUcWegNbF70CVRm2h/7xy7jQ3R9LaY4VVSvjnoVWwWVhNL60DiZsBpC5tSzYQOCvDbzncIpIjPZWodZA==", + "dependencies": { + "@types/hast": "^2.0.0", + "@types/katex": "^0.14.0", + "hast-util-from-html-isomorphic": "^1.0.0", + "hast-util-to-text": "^3.1.0", + "katex": "^0.16.0", + "unist-util-visit": "^4.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, + "node_modules/rehype-katex/node_modules/unist-util-visit": { + "version": "4.1.2", + "resolved": "https://registry.npmjs.org/unist-util-visit/-/unist-util-visit-4.1.2.tgz", + "integrity": "sha512-MSd8OUGISqHdVvfY9TPhyK2VdUrPgxkUtWSuMHF6XAAFuL4LokseigBnZtPnJMu+FbynTkFNnFlyjxpVKujMRg==", + "dependencies": { + "@types/unist": "^2.0.0", + "unist-util-is": "^5.0.0", + "unist-util-visit-parents": "^5.1.1" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/rehype-parse": { "version": "8.0.5", "resolved": "https://registry.npmjs.org/rehype-parse/-/rehype-parse-8.0.5.tgz", @@ -7018,6 +7211,39 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/remark-math": { + "version": "5.1.1", + "resolved": "https://registry.npmjs.org/remark-math/-/remark-math-5.1.1.tgz", + "integrity": "sha512-cE5T2R/xLVtfFI4cCePtiRn+e6jKMtFDR3P8V3qpv8wpKjwvHoBA4eJzvX+nVrnlNy0911bdGmuspCSwetfYHw==", + "dependencies": { + "@types/mdast": "^3.0.0", + "mdast-util-math": "^2.0.0", + "micromark-extension-math": "^2.0.0", + "unified": "^10.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, + "node_modules/remark-math/node_modules/unified": { + "version": "10.1.2", + "resolved": "https://registry.npmjs.org/unified/-/unified-10.1.2.tgz", + "integrity": "sha512-pUSWAi/RAnVy1Pif2kAoeWNBa3JVrx0MId2LASj8G+7AiHWoKZNTomq6LG326T68U7/e263X6fTdcXIy7XnF7Q==", + "dependencies": { + "@types/unist": "^2.0.0", + "bail": "^2.0.0", + "extend": "^3.0.0", + "is-buffer": "^2.0.0", + "is-plain-obj": "^4.0.0", + "trough": "^2.0.0", + "vfile": "^5.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/remark-mdx": { "version": "2.3.0", "resolved": "https://registry.npmjs.org/remark-mdx/-/remark-mdx-2.3.0.tgz", @@ -8152,6 +8378,19 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/unist-util-find-after": { + "version": "4.0.1", + "resolved": "https://registry.npmjs.org/unist-util-find-after/-/unist-util-find-after-4.0.1.tgz", + "integrity": "sha512-QO/PuPMm2ERxC6vFXEPtmAutOopy5PknD+Oq64gGwxKtk4xwo9Z97t9Av1obPmGU0IyTa6EKYUfTrK2QJS3Ozw==", + "dependencies": { + "@types/unist": "^2.0.0", + "unist-util-is": "^5.0.0" + }, + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/unified" + } + }, "node_modules/unist-util-generated": { "version": "2.0.1", "resolved": "https://registry.npmjs.org/unist-util-generated/-/unist-util-generated-2.0.1.tgz", diff --git a/package.json b/package.json index 4724264..1530bb0 100644 --- a/package.json +++ b/package.json @@ -18,11 +18,14 @@ "astro-imagetools": "^0.9.0", "astro-remark-description": "^1.0.1", "fork-awesome": "^1.2.0", + "katex": "^0.16.8", "lodash-es": "^4.17.21", "mdast-util-to-string": "^4.0.0", "reading-time": "^1.5.0", + "rehype-katex": "^6.0.3", "remark-emoji": "^4.0.0", "remark-github-beta-blockquote-admonitions": "^2.1.0", + "remark-math": "^5.1.1", "remark-parse": "^10.0.2" }, "devDependencies": { diff --git a/src/content/posts/2023-09-01-formal-cek-machine-in-agda/index.md b/src/content/posts/2023-09-01-formal-cek-machine-in-agda/index.md index 3ac442b..14ff529 100644 --- a/src/content/posts/2023-09-01-formal-cek-machine-in-agda/index.md +++ b/src/content/posts/2023-09-01-formal-cek-machine-in-agda/index.md @@ -66,21 +66,21 @@ several constructors: [lambda calculus]: https://en.wikipedia.org/wiki/Lambda_calculus -- **Var.** This is just a variable, like `x` or `y`. By itself it holds no +- **Var.** This is just a variable, like $x$ or $y$. By itself it holds no meaning, but during evaluation, the evaluation _environment_ holds a mapping - from variable names to the values. If the environment says `{ x = 5 }`, then - evaluating `x` would result in 5. + from variable names to the values. If the environment says $\{ x = 5 \}$, then + evaluating $x$ would result in $5$. -- **Abstraction, or lambda (λ).** An _abstraction_ is a term that describes some +- **Abstraction, or lambda ($\lambda$).** An _abstraction_ is a term that describes some other computation. From an algebraic perspective, it can be thought of as a - function with a single argument (i.e f(x) = 2x is an abstraction, although - it would be written `(λx.2x)`) + function with a single argument (i.e $f(x) = 2x$ is an abstraction, although + it would be written using the notation $\lambda x.2x$) - **Application.** Application is sort of the opposite of abstraction, exposing the computation that was abstracted away. From an algebraic perspective, - this is just function application (i.e applying `f(x) = 2x` to 3 would - result in 2\*3. Note that only a simple substitution has been done and - further evaluation is required to reduce 2\*3) + this is just function application (i.e applying $f(x) = 2x$ to $3$ would + result in $2 \times 3 = 6$. Note that only a simple substitution has been done + and further evaluation is required to reduce $2\times 3$) ### Why? @@ -99,20 +99,24 @@ evaluation. In fact, the lambda calculus is [Turing-complete][tc], so any computation can technically be reduced to those 3 constructs. I used numbers liberally in the examples above, but in a lambda calculus without numbers, you could define -integers using a recursive strategy called [Church numerals]. It looks like this: +integers using a recursive strategy called [Church numerals]. It works like this: [church numerals]: https://en.wikipedia.org/wiki/Church_encoding -- Let `z` represent zero. -- Let `s` represent a "successor", or increment function. `s(z)` represents 1, - `s(s(z))` represents 2, and so on. +- $z$ represents zero. +- $s$ represents a "successor", or increment function. So: + - $s(z)$ represents 1, + - $s(s(z))$ represents 2 + - and so on. In lambda calculus terms, this would look like: -- 0 = `λs.(λz.z)` -- 1 = `λs.(λz.s(z))` -- 2 = `λs.(λz.s(s(z)))` -- 3 = `λs.(λz.s(s(s(z))))` +| number | lambda calculus expression | +| ------ | ---------------------------------- | +| 0 | $\lambda s.(\lambda z.z)$ | +| 1 | $\lambda s.(\lambda z.s(z))$ | +| 2 | $\lambda s.(\lambda z.s(s(z)))$ | +| 3 | $\lambda s.(\lambda z.s(s(s(z))))$ | In practice, many lambda calculus incorporate higher level constructors such as numbers or lists to make it so we can avoid having to represent them using only @@ -129,21 +133,31 @@ a fixed-point combinator: [tc]: https://en.wikipedia.org/wiki/Turing_completeness - Y = λf.(λx.f(x(x)))(λx.f(x(x))) +$$ +Y = \lambda f.(\lambda x.f(x(x)))(\lambda x.f(x(x))) +$$ -That's quite a mouthful. If you tried calling Y on some term, you will find that -evaluation will quickly expand infinitely. That makes sense given its purpose: -to find a _fixed point_ of whatever function you pass in. +That's quite a mouthful. If you tried calling $Y$ on some term, you will find +that evaluation will quickly expand infinitely. That makes sense given its +purpose: to find a _fixed point_ of whatever function you pass in. -> As an example, the fixed-point of the function f(x) = sqrt(x) is 1. That's -> because f(1) = 1. The Y combinator attempts to find the fixed point by simply -> applying the function multiple times. In the untyped lambda calculus, this can -> be used to implement simple (but possibly unbounded) recursion. +> [!NOTE] +> As an example, the fixed-point of the function $f(x) = \sqrt{x}$ is $1$. +> That's because $f(1) = 1$, and applying $f$ to any other number sort of +> converges in on this value. If you took any number and applied $f$ infinitely +> many times on it, you would get $1$. +> +> In this sense, the Y combinator can be seen as a sort of brute-force approach +> of finding this fixed point by simply applying the function over and over until +> the result stops changing. In the untyped lambda calculus, this can be used to +> implement simple (but possibly unbounded) recursion. This actually proves disastrous for trying to reason about the logic of a -program. If we don't even know for sure if something will halt, how can we know -that it'll produce the correct value? In fact, you can prove false statements -using infinite recursion as a basis. +program. If something is able to recurse on itself without limit, we won't be +able to tell what its result is, and we _definitely_ won't be able to know if +the result is correct. This is why we typically ban unbounded recursion in +proof systems. In fact, you can give proofs for false statements using infinite +recursion. This is why we actually prefer _not_ to work with Turing-complete languages when doing logical reasoning on program evaluation. Instead, we always want to add @@ -152,26 +166,29 @@ information about our program's behavior. ### Simply-typed lambda calculus -The [simply-typed lambda calculus] (STLC) adds types to every term. Types are -crucial to any kind of static program analysis. Suppose I was trying to apply -the term 5 to 6 (in other words, call 5 with the argument 6 as if 5 was a -function). As humans we can look at that and instantly recognize that the +The [simply-typed lambda calculus] (STLC, or the notational variant +$\lambda^\rightarrow$) adds types to every term. Types are crucial to any kind +of static program analysis. Suppose I was trying to apply the term $5$ to $6$ (in +other words, call $5$ with the argument $6$ as if $5$ was a function, like +$5(6)$). As humans we can look at that and instantly recognize that the evaluation would be invalid, yet under the untyped lambda calculus, it would be completely representable. [simply-typed lambda calculus]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus To solve this in STLC, we would make this term completely unrepresentable at -all. To say you want to apply 5 to 6 would not be a legal STLC term. We do this -by requiring that all STLC terms are untyped lambda calculus terms accompanied -by a _type_. +all. To say you want to apply $5$ to $6$ would not be a legal STLC term. We do +this by requiring that all STLC terms are untyped lambda calculus terms +accompanied by a _type_. This gives us more information about what's allowed before we run the -evaluation. For example, numbers may have their own type `Nat` (for "natural -number"), while functions have a special "arrow" type `_ -> _`, where the -underscores represent other types. A function that takes a number and returns a -boolean (like isEven) would have the type `Nat -> Bool`, while a function that -takes a boolean and returns another boolean would be `Bool -> Bool`. +evaluation. For example, numbers may have their own type $\mathbb{N}$ (read +"nat", for "natural number") and booleans are $\mathrm{Bool}$, while functions +have a special "arrow" type $\_\rightarrow\_$, where the underscores represent +other types. A function that takes a number and returns a boolean (like isEven) +would have the type $\mathbb{N} \rightarrow \mathrm{Bool}$, while a function +that takes a boolean and returns another boolean would be $\mathrm{Bool} +\rightarrow \mathrm{Bool}$. With this, we have a framework for rejecting terms that would otherwise be legal in untyped lambda calculus, but would break when we tried to evaluate them. A @@ -187,28 +204,33 @@ A semi-formal definition for STLC terms would look something like this: - **Var.** Same as before, it's a variable that can be looked up in the environment. -- **Abstraction, or lambda (λ).** This is a function that carries three pieces - of information: (1) the name of the variable that its input will be substituted - for, (2) the _type_ of the input, and (3) the body in which the substitution - will happen. +- **Abstraction, or lambda ($\lambda$).** This is a function that carries three pieces + of information: + + 1. the name of the variable that its input will be substituted for + 2. the _type_ of the input, and + 3. the body in which the substitution will happen. - **Application.** Same as before. It doesn't really seem like changing just one term changes the language all that much. But as a result of this tiny change, _every_ term now has a type: -- `5 :: Nat` -- `λ(x:Nat).2x :: Nat -> Nat` -- `isEven(3) :: (Nat -> Bool) · Nat = Bool` +- $5 :: \mathbb{N}$ +- $λ(x:\mathbb{N}).2x :: \mathbb{N} \rightarrow \mathbb{N}$ +- $isEven(3) :: (\mathbb{N} \rightarrow \mathrm{Bool}) · \mathbb{N} = \mathrm{Bool}$ -Notation: (`x :: T` means `x` has type `T`, and `f · x` means `f` applied to -`x`) +> [!NOTE] +> Some notation: +> +> - $x :: T$ means $x$ has type $T$, and +> - $f · x$ means $f$ applied to $x$ This also means that some values are now unrepresentable: -- `isEven(λx.2x) :: (Nat -> Bool) · (Nat -> Nat)` doesn't work because the type - of `λx.2x :: Nat -> Nat` can't be used as an input for `isEven`, which is - expecting a `Nat`. +- $isEven(λx.2x)$ wouldn't work anymore because the type of the inner argument + $λx.2x$ would be $\mathbb{N} \rightarrow \mathbb{N}$ can't be used as an input + for $isEven$, which is expecting a $\mathbb{N}$. We have a good foundation for writing programs now, but this by itself can't qualify as a system for computation. We need an abstract machine of sorts that diff --git a/src/layouts/BaseLayout.astro b/src/layouts/BaseLayout.astro index 274d8a7..7805859 100644 --- a/src/layouts/BaseLayout.astro +++ b/src/layouts/BaseLayout.astro @@ -2,6 +2,7 @@ import Footer from "../components/Footer.astro"; import LeftNav from "../components/LeftNav.astro"; import "../styles/global.scss"; +import "katex/dist/katex.min.css"; --- diff --git a/src/styles/post.scss b/src/styles/post.scss index 7bfa09f..c715fbe 100644 --- a/src/styles/post.scss +++ b/src/styles/post.scss @@ -160,9 +160,12 @@ table { border-collapse: collapse; + border: 1px solid var(--hr-color); + border-radius: 4px; thead { - background-color: black; + background-color: var(--hr-color); + // color: var(--background-color); } td, @@ -239,10 +242,9 @@ hr.endline { .admonition-title { color: var(--color); - margin-bottom: 6px; } p { - margin: 0; + margin: 8px auto; } }