From ed8c2d6b56655f1a362f7683b9da3ac521920a42 Mon Sep 17 00:00:00 2001 From: JJ Date: Sun, 19 May 2024 20:04:59 -0700 Subject: meow --- computation/index.md | 2 +- linguistics/semantics.md | 4 ++-- mathematics/information-theory.md | 6 ++++++ plt/continuations.md | 10 ++++++++-- plt/index.md | 26 ++++++++++++++++++++++++++ plt/interaction-nets.md | 11 +++++++++++ plt/lambda-calculus.md | 20 ++++++++++++++++++++ 7 files changed, 74 insertions(+), 5 deletions(-) create mode 100644 mathematics/information-theory.md create mode 100644 plt/interaction-nets.md diff --git a/computation/index.md b/computation/index.md index e1a6818..ce13a58 100644 --- a/computation/index.md +++ b/computation/index.md @@ -8,4 +8,4 @@ title: computation

-# computation and its consequences +# computation is *well-defined* execution diff --git a/linguistics/semantics.md b/linguistics/semantics.md index 96638aa..a6cb615 100644 --- a/linguistics/semantics.md +++ b/linguistics/semantics.md @@ -42,8 +42,8 @@ With basic logic and the lambda calculus under our belt, we may simply get strai > *Alice is bad.*
> *The blue pigeon flew away.* -- Noun $↝ λx.Noun(x)$ $: ⟨e,t⟩$ -- Verb (intransitive) ↝ $λx.Verb(x)$: $⟨e,t⟩$ +- Noun: $⟨e,t⟩ ↝ λx.Noun(x)$ +- Verb (intransitive): $⟨e,t⟩ ↝ λx.Verb(x)$ - Verb (transitive): $⟨e,⟨e,t⟩⟩ ↝ λy.λx.Verb(x, y)$ - Verb (meaningless): $⟨⟨e,t⟩,⟨e,t⟩⟩ ↝ λP.λx.P(x)$ - Adj: $⟨⟨e,t⟩,⟨e,t⟩⟩ ↝ λNoun.λx.[Adj(x) ∧ Noun(x)]$ diff --git a/mathematics/information-theory.md b/mathematics/information-theory.md new file mode 100644 index 0000000..d0cd75c --- /dev/null +++ b/mathematics/information-theory.md @@ -0,0 +1,6 @@ +--- +layout: mathematics +title: mathematics/information theory +--- + +# information theory diff --git a/plt/continuations.md b/plt/continuations.md index b1566d0..096e0c3 100644 --- a/plt/continuations.md +++ b/plt/continuations.md @@ -5,12 +5,18 @@ title: computation/continuations # continuations -- [nim-works CPS](https://github.com/nim-works/cps/tree/master/docs): +- ✨ [Deliminated Continuations, Demystified](https://www.youtube.com/watch?v=TE48LsgVlIU): 45-minute talk explaining native first-class deliminated continuations - and everything else along the way +- ✨ [Oleg Kiselyov's writings](https://okmij.org/ftp/continuations/) +- [nim-works CPS](https://github.com/nim-works/cps/tree/master/docs) - [CPS vs. SSA](http://www.mlton.org/pipermail/mlton/2003-January/023054.html) - [By example: continuation-passing style](https://matt.might.net/articles/by-example-continuation-passing-style/) - [How to compile with continuations](https://matt.might.net/articles/cps-conversion/) -- [**Oleg Kiselyov's writings**](https://okmij.org/ftp/continuations/) - [An argument against call/cc](https://okmij.org/ftp/continuations/against-callcc.html) +- [Compiling with Continuations](https://annas-archive.org/md5/ce6c60adc8597d750a1f2b7f5023e207) +- [The Essence of Compiling with Continuations](https://dl.acm.org/doi/pdf/10.1145/173262.155113) +- [Compiling with Continuations, Continued](../papers/1291151.1291179.pdf) +- [Compiling without Continuations](https://dl.acm.org/doi/pdf/10.1145/3062341.3062380) +- [Compiling with Continuations, or without? Whatever.](https://dl.acm.org/doi/pdf/10.1145/3341643) ## continuations diff --git a/plt/index.md b/plt/index.md index 8cd6a05..2f5da20 100644 --- a/plt/index.md +++ b/plt/index.md @@ -3,4 +3,30 @@ layout: plt title: programming language theory --- +
+
+
+
+
+ # programming language theory + +constructs +- [types](types) +- [continuations](continuations) +- [effects](effects) +- [modules](modules) +- monads + +formalisms +- syntax +- semantics +- formal verification +- paradigms + +computation +- propositions as types +- [the lambda calculus](lambda-calculus) +- turing machines +- [interaction nets](interaction-nets) +- combinators diff --git a/plt/interaction-nets.md b/plt/interaction-nets.md new file mode 100644 index 0000000..c5ce362 --- /dev/null +++ b/plt/interaction-nets.md @@ -0,0 +1,11 @@ +--- +layout: plt +title: computation/interaction nets +--- + +# interaction nets + +- [xxiivv](https://wiki.xxiivv.com/site/interaction_nets.html) +- [Interaction nets](https://dl.acm.org/doi/pdf/10.1145/96709.96718) +- [An algorithm for optimal lambda calculus reduction](https://dl.acm.org/doi/pdf/10.1145/96709.96711) +- [Optimality and inefficiency: what isn't a cost-model of the lambda calculus?](https://dl.acm.org/doi/pdf/10.1145/232629.232639) diff --git a/plt/lambda-calculus.md b/plt/lambda-calculus.md index b666ef6..7d15dbf 100644 --- a/plt/lambda-calculus.md +++ b/plt/lambda-calculus.md @@ -4,3 +4,23 @@ title: computation/lambda calculus --- # the lambda calculus + +the lambda calculus is a simple expression of computation. + +```racket +;; A full implementation of the untyped lambda calculus in Racket. +(define (interpret expr [ctx #hash()]) + (match expr + [val #:when (value? val) val] + [val #:when (symbol? val) + (if (dict-has-key? ctx val) + (interpret (dict-ref ctx val) ctx) val)] + [`(λ ,id ,body) `(λ ,id ,body)] + [`(,body ,arg) + (match (interpret body ctx) + [`(λ ,id ,body) (interpret body (dict-set ctx id (interpret arg ctx)))] + [expr `(,(interpret expr ctx) ,(interpret arg ctx))])] + [expr (error (format "invalid expression ~a" expr))])) +``` + +in computer science, the lambda calculus is often used as a base for languages and types systems for its simplicity and extended with syntax and types of various fashions. in linguistics, the lambda calculus is used for its compact notation of functions and is often extended with quantifiers and abstract functions. in mathematics, the lambda calculus is studied in its own right. -- cgit v1.2.3-70-g09d2