The #LambdaCalculus is Algebraic
https://www.mscs.dal.ca/~selinger/papers/combinatory.pdf …pic.twitter.com/wp2SRSkAtE
-
Introduction seems a bit off to me. Algebraic models of lambda calculi are known already, including treatment of binders and substitutions, and in a way which doesn't need combinators. E.g.: https://arxiv.org/abs/1904.00827
this is two different senses of the word "algebraic". the introduction to the paper is entirely correct! the lambda-calculus as usually constructed cannot be given as an equationally presentable class of algebras. the fact that you can give it a model in a cwf is distinct...
-
-
saying "in a way which doesn't need combinators" misses the point. the reason one uses combinators is because they correspond to a certain class of equational theories which are called "algebraic"! so the lambda calculus, in the usual style, is not e.g. a lawvere theory.
-
the very nice paper you linked explains how it corresponds to a _richer_ thing called a "generalized algebraic theory" -- but the reason it does is that gats have a theory of binding and substitution _built in_!
- Još 5 drugih odgovora
Novi razgovor -
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.