New answers tagged lambda-calculus
1
vote
Must the evaluation strategy for a language be specified in order to apply the Church-Rosser Theorem?
The Church-Rosser theorem gives you the following guarantees:
A term has at most one normal form. That is, there aren't different normal forms depending on your choice of evaluation strategy.
If a ...
0
votes
Is there a hierarchy of computational expressivity that is sensitive to evaluation strategies?
Most (or all) reasonable programming are Turing-complete, and thus can be used to compute exactly the computable functions, i.e., to decide the decidable languages, nothing more and nothing less. So ...

D.W.♦
- 143k
Top 50 recent answers are included
Related Tags
lambda-calculus × 510functional-programming × 80
type-theory × 63
logic × 42
programming-languages × 39
combinatory-logic × 39
computability × 25
turing-machines × 23
types-and-programming-languages × 23
terminology × 19
semantics × 18
computation-models × 17
category-theory × 17
type-inference × 17
term-rewriting × 16
turing-completeness × 13
evaluation-strategies × 12
church-numerals × 12
formal-grammars × 11
reference-request × 11
dependent-types × 11
type-checking × 11
variable-binding × 10
complexity-theory × 8
reductions × 8