diff options
author | joseville1001 <66519798+joseville1001@users.noreply.github.com> | 2021-11-14 06:40:54 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-14 12:40:54 +0100 |
commit | e6f3c19425a4f7280323c8815073f9a489b83652 (patch) | |
tree | 6be64b80e286b8eacf0ab270e517f21907ee939f | |
parent | 519ad03a55cd0577f5d0d09d5606607116ff32c9 (diff) |
nit: Add caveat to rule 2. `λx.c = Kc` (#4267)
See this math stackexchange Q/A for the reason why this caveat is important: https://math.stackexchange.com/questions/4304294/rules-for-converting-lambda-calculus-expressions-to-ski-combinator-calculus-expr.
(There may be other clearer ways of wording the caveat. It is also not necessary that the caveat be shown inline with the rules; an alternative is to use a footnote or to make a note below the rules.)
-rw-r--r-- | lambda-calculus.html.markdown | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lambda-calculus.html.markdown b/lambda-calculus.html.markdown index 53a7a7cd..958dd746 100644 --- a/lambda-calculus.html.markdown +++ b/lambda-calculus.html.markdown @@ -131,7 +131,7 @@ We can convert an expression in the lambda calculus to an expression in the SKI combinator calculus: 1. `λx.x = I` -2. `λx.c = Kc` +2. `λx.c = Kc` provided that `x` does not occur free in `c` 3. `λx.(y z) = S (λx.y) (λx.z)` Take the church number 2 for example: |