Questions tagged [extensionality]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0 votes
0 answers
168 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 ...
MaiaVictor's user avatar
  • 3,137
6 votes
1 answer
203 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 ...
ice1000's user avatar
  • 965
1 vote
0 answers
343 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 ...
Turbo's user avatar
  • 12.8k
12 votes
1 answer
351 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 ...
Jonathan Gallagher's user avatar
2 votes
2 answers
269 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}\...
N. Virgo's user avatar
  • 699
3 votes
0 answers
60 views

Functionality of a hierarchy of definable functions over $\mathbb{N}$

Let $T$ be the complete hierarchy of functions over $\mathbb{N}$. That is: $T$ = $\bigcup T_{\tau}$ for all simple types $\tau$ built up from the basic type $\mathbb{N}$, with $T_{\mathbb{N}} = \...
Cian's user avatar
  • 131
14 votes
4 answers
878 views

Is eta-equivalence for functions compatiable with Haskell's seq operation?

Lemma: Assuming eta-equivalence we have that (\x -> ⊥) = ⊥ :: A -> B. Proof: ⊥ = (\x -> ⊥ x) by eta-equivalence, and <...
Russell O'Connor's user avatar
9 votes
3 answers
1k views

Is it possible to compute whether two functions are extensional equal?

If you have two functions implementing a different sorting algorithm, is it then possible to infer by source code that they both have the same external properties? Meaning that they both will have a ...
Matthijs Steen's user avatar
11 votes
1 answer
527 views

Extensionality of lambda calculus models

I'm translating a book on LISP and naturally it touches some elements of $\lambda$-calculus. So, a notion of extensionality is mentioned there alongside some models of $\lambda$-calculus, namely: $\...
Chris's user avatar
  • 113
23 votes
4 answers
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 ...
Trylks's user avatar
  • 604
15 votes
2 answers
512 views

Are there intermediate eta theories for the lambda calculus?

There are two main, studied theories of the lambda calculus, the beta theory and its Post-complete extension, the beta-eta theory. Do these two theories have an in-between, a kind of intermediate eta ...
Charles Stewart's user avatar