Why are there two not operators in lambda calculus? - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2021-12-02T23:04:46Z https://cs.stackexchange.com/feeds/question/102290 https://creativecommons.org/licenses/by-sa/4.0/rdf https://cs.stackexchange.com/q/102290 4 Why are there two not operators in lambda calculus? HappyFace https://cs.stackexchange.com/users/87634 2019-01-02T15:14:27Z 2019-01-03T00:11:01Z <p>From <a href="https://en.wikipedia.org/w/index.php?title=Church_encoding&amp;oldid=874761158#Church_Booleans" rel="nofollow noreferrer">Wikipedia</a>:</p> <blockquote> <p><span class="math-container">$\mathrm{true} = \lambda a. \lambda b. a$</span><br /> <span class="math-container">$\mathrm{false} = \lambda a. \lambda b. b$</span></p> <p>Because true and false choose the first or second parameter they may be combined to provide logic operators. Note that there are two version of not, depending on the evaluation strategy that is chosen.</p> <p><span class="math-container">$\mathrm{and} = \lambda p . \lambda q . p \, q \, p$</span><br /> <span class="math-container">$\mathrm{or} = \lambda p . \lambda q . p \, p \, q$</span></p> <p><span class="math-container">$\mathrm{not}_A = \lambda p . \lambda a . \lambda b . p \, b \, a$</span>   (This is only a correct implementation if the evaluation strategy is applicative order.)</p> <p><span class="math-container">$\mathrm{not}_N = \lambda p . p \, (\lambda a . \lambda b . b) \, (\lambda a . \lambda b . a) = \lambda p . p \, \mathrm{false} \, ⁡\mathrm{true}⁡$</span>   (This is only a correct implementation if the evaluation strategy is normal order.)</p> </blockquote> <p>I know what applicative order and normal order are (eager evaluation vs lazy evaluation of arguments to functions). But I don’t understand why the two nots don’t work in both of these evaluation strategies.</p> https://cs.stackexchange.com/questions/102290/-/102308#102308 4 Answer by Gilles 'SO- stop being evil' for Why are there two not operators in lambda calculus? Gilles 'SO- stop being evil' https://cs.stackexchange.com/users/39 2019-01-02T23:50:10Z 2019-01-03T00:11:01Z <p>The lambda-calculus is confluent. All the terms involved are strongly normalizing (these boolean encodings only work on booleans; they could do anything if applied to a lambda-term that doesn't reduce to <span class="math-container">$\mathrm{true}$</span> or <span class="math-container">$\mathrm{false}$</span>). So the choice of reduction strategy is not relevant.</p> <hr> <p>When something looks weird or incomprehensible on Wikipedia, check the history. Sometimes things get deformed over successive edits, and sometimes an edit is just wrong. <a href="https://en.wikipedia.org/wiki/Wikipedia:WikiBlame" rel="nofollow noreferrer">WikiBlame</a> can be very useful for that.</p> <p>The edit that introduced the distinction between two evaluation strategy is <a href="https://en.wikipedia.org/w/index.php?title=Church_encoding&amp;diff=prev&amp;oldid=511250377" rel="nofollow noreferrer">from September 2012</a>. It has no edit description, its content doesn't make sense (it implies that call-by-value is not an applicative-order strategy), and even the author was clearly not sure what they wrote (they left a comment with an interrogation).</p> <p>The bit about normal order was added in <a href="https://en.wikipedia.org/w/index.php?diff=584592755&amp;oldid=584591579&amp;title=Church_encoding" rel="nofollow noreferrer">December 2013</a> which was part of a series of edits mainly to improve the formatting and the wording. It doesn't look to me like the editor meant to change the meaning of the article, but they were mislead by the previous edit.</p> <p>Hopefully someone will soon edit this article to rectify it, ideally with references for both of the not functions.</p> <hr> <p>Incidentally, the choice of reduction strategy does matter if you want to extend these functions outside the booleans. For example, if you want to have <span class="math-container">$\mathrm{if}\,b\,M\,N$</span> where <span class="math-container">$b$</span> is a boolean (a term that reduces to <span class="math-container">$\mathrm{true}$</span> or <span class="math-container">$\mathrm{false}$</span>) and <span class="math-container">$M$</span> and <span class="math-container">$N$</span> are arbitrary terms, then this behaves differently depending on the evaluation strategy. With call-by-value, this only terminates if <span class="math-container">$M$</span> and <span class="math-container">$N$</span> terminates. With call-by-name, this terminates if whichever of <span class="math-container">$M$</span> or <span class="math-container">$N$</span> is selected terminates, and the one that isn't selected doesn't matter. This is the reason why <code>if</code> can be defined as a function in languages that use call-by-name or lazy evaluation such as Haskell, but it needs to be a special form in languages that use eager evaluation such as Lisp and ML.</p> <p>Another case where the evaluation strategy matters is if you want to work on <em>partial</em> booleans, that is, terms that either reduce to one of <span class="math-container">$\mathrm{true}$</span> or <span class="math-container">$\mathrm{false}$</span> or don't terminate (<span class="math-container">$\bot$</span>). For <span class="math-container">$\mathrm{not}$</span>, the choice of evalation strategy doesn't matter: <span class="math-container">$\mathrm{not}\,\bot = \bot$</span> anyway. For an operator like <span class="math-container">$\mathrm{or}$</span>, the evaluation order does matter: <span class="math-container">$\mathrm{or} \, \mathrm{true} \, \bot$</span> could be either <span class="math-container">$\mathrm{true}$</span> or <span class="math-container">$\bot$</span>, and likewise for <span class="math-container">$\mathrm{or} \, \bot \, \mathrm{true}$</span>. With eager evaluation, they're both <span class="math-container">$\bot$</span>, but with left-to-right normal order <span class="math-container">$\mathrm{or} \, \mathrm{true} \, \bot \to \mathrm{true}$</span> while <span class="math-container">$\mathrm{or} \, \bot \, \mathrm{true}$</span> does not terminate. It's natural to wonder if there could be a more clever implementation of <span class="math-container">$\mathrm{or}$</span> that always picks its terminating argument regardless of the evaluation strategy. This problem is known as <a href="http://homepages.inf.ed.ac.uk/gdp/publications/LCF.pdf" rel="nofollow noreferrer">Plotkin's parallel or</a>, and it's an important result in the theory of the lambda calculus that there is no such term. There is no way for a lambda calculus function to take two arguments and evaluate them “in parallel”, reducing them and stopping as soon as one of them terminates. The function can be weakly normalizing (it terminates in some evaluation strategies) but not strongly normalizing (there are evaluation strategies where it doesn't terminate). Thus the lambda calculus is said to be <em>inherently sequential</em>. It's a very nice model of sequential computation, but if you want to model parallelism or concurrency, you need other tools.</p>