Questions tagged [hereditary-substitution]
Hereditary substitution is an algorithm that directly computes the canonical result of an ordinary substitution of one canonical form into another. (from Twelf)
3
questions
2
votes
1
answer
196
views
Conflicting terminology for completeness/soundness of normalization algorithm
While reading some articles about formalization of various normalization algorithms, I found that these two papers use the term completeness/soundness in opposite way.
Hereditary Substitutions for ...
- 123
2
votes
2
answers
189
views
Canonical forms of combinators
Binders are painful when dealing with metatheory. Combinators are one potential approach to avoid the pain of binders. But it'd be nice if I could normalize combinators to canonical forms. Is there ...
- 2,868
12
votes
2
answers
567
views
What is hereditary substitution and why should I use it?
What is hereditary substitutio,n and why should I use it?
I've been taking a look at hereditary substitution for my little programming language, because hereditary substitution is supposed to give a ...
- 2,868