# Questions tagged [extensionality]

The tag has no usage guidance.

9 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 <...
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 ...
471 views

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: $\... 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 ... 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}} = \...
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}\...