summaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorjoseville1001 <66519798+joseville1001@users.noreply.github.com>2021-11-14 06:40:54 -0500
committerGitHub <noreply@github.com>2021-11-14 12:40:54 +0100
commite6f3c19425a4f7280323c8815073f9a489b83652 (patch)
tree6be64b80e286b8eacf0ab270e517f21907ee939f
parent519ad03a55cd0577f5d0d09d5606607116ff32c9 (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.markdown2
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: