Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [extensionality]

The tag has no usage guidance.

11
votes
1answer
142 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
1answer
119 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
0answers
51 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
4answers
532 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
3answers
618 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 ...
10
votes
1answer
369 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: $\...
17
votes
4answers
2k 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
432 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 ...