I actually wrote a bit about this on my website: https://azdavis.net/posts/lambda-cube/
I’ve been using my website as a way to practice writing, so please let me know what you think.
I’ve been using my website as a way to practice writing, so please let me know what you think.
There’s actually no JS on my site at load time, I run it all as a build step that transforms Markdown with inline LaTeX into pure HTML and CSS. https://github.com/azdavis/azdavis.net
Thank you
`t ::= ...` is saying "A CoC term, called t, can have the following forms ..." Then each case is separated by `|`.
The cases for application, abstraction, and forall are recursive, in that they contain t (or t') when the thing being defined is also called t. (The prime on t' is just to say that t and t' can be different terms.)
So for instance, the case for application is:
t(t')
That means if you already have two arbitrary CoC terms, called t and t', then if you write down first the term t, then a `(`, then the term t', then a `)`, then you've written down another CoC term representing the application of the term t to the term t'.
And the case for abstraction is
λ(x:t) t'
That means if you have two CoC terms t and t', then if you write down `λ`, then `(`, then a variable name (x is kind of a meta-variable-placeholder name, you can name the variable whatever you want), then `:`, then the term t, then `)`, then the term t', then you've written down an abstraction term. In this case, the variable x (or whatever you called it) has type t, and can appear free in t'.
> interesting tangents
Yeah, I’ve found that explaining things by first giving an example and then generalizing often works better than trying to start with raw theory.