Last call to make your voice heard! Our 2022 Developer Survey closes in less than a week. Take survey.

# Questions tagged [extensionality]

The tag has no usage guidance.

11 questions
Filter by
Sorted by
Tagged with
136 views

### What is wrong with the "obvious" approach to function extensionality by providing context-aware rewrites?

There is an obvious, dirty and probably wrong approach that allows one to prove function extensionality in a straight-forward manner: provide an equality primitive with a context-aware rewrite. For ...
• 3,045
165 views

### What is the general definition of 'extensionality' in type theory and how is extensionality defined for positive types?

It is well-known in the literature that (internal) extensionality of a function type means $(\prod_a f~a=g~a)\implies f=g$ (where $=$ is the intensional equality type) and extensionality of a product ...
• 923
1 vote
244 views

### Does simplex algorithm run in polynomial on Bipartite Perfect matching polytope?

It is well known that simplex algorithm runs in exponential time in worst case. However are there situations (necessary and sufficient conditions) where simplex algorithm runs in polynomial time? In ...
• 12.5k
304 views

### Eta expansion in the pattern lambda calculus

Klop, van Oostrom, and de Vrijer have a paper on the lambda calculus with patterns. http://www.sciencedirect.com/science/article/pii/S0304397508000571 In some sense, a pattern is a tree of variables ...
197 views

### Algorithm for extensional equality in combinator calculus

I'm dealing with combinator calculus, using the $S$ and $K$ combinators as a basis. Sometimes my code generates expressions that define equivalent functions, such as  (S\, K\, K) \qquad\text{and}\...
• 679
53 views

• 113
4k views

### What's the point of $\eta$-conversion in lambda calculus?

I think I'm not understanding it, but $\eta$-conversion looks to me as a $\beta$-conversion that does nothing, a special case of $\beta$-conversion where the result is just the term in the lambda ...
• 584