New answers tagged lambda-calculus
4
votes
Does anything go wrong in the lambda cube if we forbid reductions of the bodies of abstractions?
For an example of reduction under binders specific to the minimal pure type systems you were asking about, the counterexample has to involve the conversion rule, because that's where beta reduction is ...
- 675
1
vote
Accepted
In the wikipedia article on the Lambda cube, does the Application rule apply to all terms or just to variables?
$a$ stands for a term. It's a metavariable, if you like, while $x$ is a variable.
- 306
2
votes
Accepted
In the Conversion inference rule of the lambda cube, why is Γ ⊢ B':s necessary?
Generally speaking, a desirable property of type theory is that a judgement like $\Gamma \vdash t : A$ can only hold if the presupposition that $A$ is a valid type in context $\Gamma$ holds, which in ...
- 306
3
votes
Accepted
How to reduce a term to normal form
Your reductions are correct. The way you pass this into the online calculators is not. You need a space between variables.
If you type (λx.λy.xy)y(xλz.zz), 'xy' is interpreted as its own variable and ...
- 156
Top 50 recent answers are included