11
votes
Accepted
What is hereditary substitution and why should I use it?
First, eta for sums is not feasible, if you want to avoid quotients or conversion relations. I don't know about any description of eta-normal forms for sum types in the literature; the closest are &...
- 2,077
7
votes
Accepted
Canonical forms of combinators
Combinators all have a predefined arity, and normal forms consist of underapplied combinators, whose arguments are normal forms. This is different from lambda calculi, where you also need neutral ...
- 4,344
7
votes
What is hereditary substitution and why should I use it?
Just a note about sum types: it's fair to say that eta for sums is not yet tractable, but I'd strongly disagree with the claim that it's practically infeasible in general.
Regardless of whether they ...
- 2,083
6
votes
Accepted
Conflicting terminology for completeness/soundness of normalization algorithm
Both answers are correct.
Soundness in general means “nothing bad happens”. In the context of equational theories, the following would be sound phenomena:
A theory is sound (with respect to a given ...
- 11k
Only top scored, non community-wiki answers of a minimum length are eligible