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 ...
user avatar
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 ...
user avatar
  • 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....
user avatar
  • 26.6k

Only top scored, non community-wiki answers of a minimum length are eligible