Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more
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 ...
Neel Krishnaswami's 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 ...
Trebor's user avatar
  • 345
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....
Andrej Bauer's user avatar
1 vote

Algorithm for extensional equality in combinator calculus

If either of two combinator terms has a strong normal form, and are η-equivalent when treated as λ-terms, then they will both have a strong normal form, it will be the same one, and it may be found by ...
NinjaDarth's user avatar

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