Skip to content

Commit

Permalink
add link to lambda graphical notations overview
Browse files Browse the repository at this point in the history
  • Loading branch information
tromp committed Feb 6, 2024
1 parent 22c2b57 commit ac6ec81
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 3 deletions.
6 changes: 3 additions & 3 deletions cl/Binary_lambda_calculus
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,8 @@ Originally, Turing machines, the most well known formalism for computation, were
Binary strings in BLC

BLC represents bits 0 and 1 are as the standard lambda booleans B0 = True and B1 = False:
True = \lambda x\, \lambda y.\, x
False = \lambda x\, \lambda y.\, y
B0 = \lambda x0\, \lambda x1.\, x0 = True
B1 = \lambda x0\, \lambda x1.\, x1 = False
which can be seen to directly implement the if-then-else operator.
The standard pairing function
\langle,\rangle = \lambda x \,\lambda y \,\lambda z.\, z x y
Expand Down Expand Up @@ -96,7 +96,7 @@ The program
(\lambda 1 1) (\lambda \lambda \lambda 1 (\lambda 1 (3 (\lambda \lambda 1)) (4 4 (\lambda 1 (\lambda \lambda \lambda 1 (\lambda 4 (\lambda \lambda 5 2 (5 2 (3 1 (2 1)))))) 4 (\lambda 1))))) (\lambda \lambda \lambda 1 (3 ((\lambda 1 1) (\lambda \lambda \lambda \lambda 1 (\lambda 5 5 (\lambda \lambda 3 5 6 (\lambda 1 (\lambda \lambda 6 1 2) 3)) (\lambda \lambda 5 (\lambda 1 4 3))) (3 1)) (\lambda \lambda 1 (\lambda \lambda 2) 2) (\lambda 1)) (\lambda \lambda 1)) 2)
proves that
KP(x) \leq \ell(\overline{x})+338
where \overline{x} is the Levenstein code for x defined by
where \overline{x} is the Levenshtein code for x defined by
\begin{array}{ll}\overline{0} & = 0 \\\overline{n+1} & = 1\ \overline{\ell(n)}\ n\\\end{array}
in which we identify numbers and bitstrings according to lexicographic order. This code has the nice property that for all k,
\ell(\overline{n}) \leq \ell(n)+\ell(\ell(n))+\cdots+ \ell^{k-1}(n) + O(\ell^k(n))
Expand Down
1 change: 1 addition & 0 deletions cl/diagrams.html
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,7 @@ <h2> Related work</h2>
which partly inspired this page.
<p>
In his <a href="http://bntr.planet.ee/lambda/work/visual_lambda.pdf">Master thesis</a>, Viktor Massal&otilde;gin discusses 4 existing graphical notations before introducing his own "bubble" notation. Figure 3 on page 10 shows 4 depictions of the fixpoint combinator (which differs from Y above in one beta reduction), while the bubble form is in Figure 5 on page 13.
<p> Prathyush Pramod compiled a <a href="https://github.com/prathyvsh/lambda-calculus-visualizations">catalogue</a> of all known graphical notations.

<h3>Note</h3>

Expand Down

0 comments on commit ac6ec81

Please sign in to comment.