Skip to main content
11 votes

What are pertinent references to cite on Scott domains?

I asked Dana Scott who kindly responded. I am relaying his answer: I think the paper “A type-theoretical alternative to ISWIM, CUCH, OWHY” answers the questions and gives the context of the discovery....
Andrej Bauer's user avatar
  • 28.9k
9 votes

Example of a term in system F which is not typable in the simply typed lambda calculus

Reacting to the previous answers, I think this is the simplest self-application which only contains types which have closed inhabitants. $$\lambda\,(f\,:\,\forall\,\alpha.\,\alpha\to\alpha).\,f\,(\...
András Kovács's user avatar
7 votes

What are pertinent references to cite on Scott domains?

First papers Scott (1993), A type-theoretical alternative to ISWIM, CUCH, OWHY. This 1969 manuscript was later published in TCS. The title is a bit odd but it seems to hide the very first written ...
7 votes

Smallest possible universal combinator

The smallest basis is the single point combinator A = λx λy λz. x z (y (λ_.z)) of size 4 abstractions + 3 applications, and of minimal size 26 bits in the binary lambda calculus. Minimal ...
John Tromp's user avatar
7 votes

Example of a term in system F which is not typable in the simply typed lambda calculus

Damiano Mazza's example uses an uninhabited type, $∀ X ⋅ X$. It is correct, but raises the obvious question whether one can do without. Here is an example that I find quite natural: $$Λ \ A B ⋅ λ \ (p ...
Jean Abou Samra's user avatar
7 votes
Accepted

Example of a term in system F which is not typable in the simply typed lambda calculus

Every normal term may be typed in system F (I can't seem to find a reference now, I'll come back with one when I have some more time). So, for example, letting $A:=\forall X.X$, then $$x^A(A\to\alpha)...
Damiano Mazza's user avatar
4 votes
Accepted

Is beta normalization used for program optimization?

Short answer: $\beta$-reduction is done like crazy in any modern optimizing compiler. As you can easily check e.g. for GHC. The caveat is that $\lambda$s usually serve no useful purpose in the ...
cody's user avatar
  • 13.9k
4 votes

Locally nameless representation implementation

Locally nameless discipline is important when one has to normalize expressions with free variables. This happens in dependent type theories, where equality of types is tangled up with equality of ...
Andrej Bauer's user avatar
  • 28.9k
4 votes

Is there a full abstraction result for an untyped lambda calculus?

Full abstraction means that denotational equality coincides with observational equivalence (under all contexts), but that notion depends on what observations you choose. If your observation on a term ...
Lê Thành Dũng 'Tito' Nguyễn's user avatar
3 votes

A few questions about ISWIM

I was around when ISWIM was being formulated, including an implementation project on the Univac 1107 in the mid 1960s. It never struck me that there were no anonymous functions. But functions were ...
orcmid's user avatar
  • 161
2 votes

deciding $\beta$-equality of planar lambda terms

If this proof sketch turns out to be correct, then β-equality of planar λ-terms is still P-complete. (Joint work by Anupam Das, Damiano Mazza, Noam Zeilberger and me; it's not yet peer-reviewed, and ...
Lê Thành Dũng 'Tito' Nguyễn's user avatar
2 votes

(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?

Yes, via Ordinary Differential Equations. Bournez et al. described a connection between Turing Machines and Ordinary Differential Equations (ODE). Such connection preserves the notion of polynomiality ...
HeMath's user avatar
  • 21
2 votes

Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic

How “standard” is it? A post by Anupam Das on the proof theory blog attacks the folklore by comparing the following two results: Proposition 1 (Folklore). For any theorem A of IPL, we can compute a ...
gadmm's user avatar
  • 307
1 vote
Accepted

What is the type of the lambda term $\lambda a.a(\lambda yt.t)(ya)$?

Be careful: the two $y$ aren't “the same”, there's a bound one and a free one. You should first perform an α-equivalence step to rename the former: $$\lambda a.a(\lambda yt.t)(ya) =_α λa.a(λzt.t)(ya). ...
sparusaurata's user avatar
1 vote

Algorithm for extensional equality in combinator calculus

If either of two combinator terms has a strong normal form, and are η-equivalent when treated as λ-terms, then they will both have a strong normal form, it will be the same one, and it may be found by ...
NinjaDarth's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible