Questions tagged [extensionality]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
19
votes
4answers
3k 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 ...
15
votes
2answers
491 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 ...
14
votes
4answers
737 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 <...
12
votes
1answer
264 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 ...
11
votes
1answer
471 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: $\...
9
votes
3answers
894 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 ...
3
votes
0answers
53 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}} = \...
2
votes
1answer
178 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}\...
1
vote
0answers
201 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 ...