Questions tagged [extensionality]
The extensionality tag has no usage guidance.
11
questions
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 ...
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 ...
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 ...
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 ...
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}\...
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}} = \...
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 <...
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 ...
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: $\...
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 ...
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 ...