{"body":"\"The trivialization can be avoided if one disrupts these suppositions: rather than marking subterms not to be evaluated by means of an evaluation-suppressing context, mark subterms that are to be evaluated, by means of an evaluation-inducing context; and introduce different syntax for a cons-cell than for an application, so that evaluation becomes clearly separate from β-reduction. To illustrate the general method, here are a series of straightforward successive alterations to pure λ-calculus, each of which evidently preserves its equational strength, at the end of which sequence the result is a pure calculus, called vau-calculus.\"","name":"","extension":"txt","url":"https://www.irccloud.com/pastebin/SAE2ND1L","modified":1631335834,"id":"SAE2ND1L","size":641,"lines":1,"own_paste":false,"theme":"","date":1631335834}