7
votes
Eta expansion in the pattern lambda calculus
This is not a complete answer; it is a comment that got too large.
If you extend typed lambda calculus with products with projective eliminators (ie, product eliminators ...
- 31.6k
6
votes
Accepted
What is the general definition of 'extensionality' in type theory and how is extensionality defined for positive types?
Extensionality is basically the reversibility of the introduction rule. Negative types have reversible introduction rules, while positive types have reversible elimination rules. So you are looking in ...
- 251
5
votes
Accepted
Algorithm for extensional equality in combinator calculus
Equality of terms in the combinator calculus is undecidable. We can encode the natural numbers as Church numerals and then show that every recursive function is represented, see for instance section 1....
- 26.6k
Only top scored, non community-wiki answers of a minimum length are eligible