Damiano Mazza
  • Member for 8 years, 1 month
  • Last seen more than a week ago
What is the contribution of lambda calculus to the field of theory of computation?
22 votes

Apart from the foundational role of the $\lambda$-calculus, which was mentioned in all other answers, I would like to add something on What exactly did the lambda calculus do to advance the theory ...

View answer
How to make the Lambda Calculus strong normalizing without a type system?
Accepted answer
22 votes

I can think of a few possible answers coming from linear logic. The simplest one is the affine lambda-calculus: consider only lambda-terms in which every variable appears at most once. This ...

View answer
Can typed lambda calculi express *all* algorithms below a given complexity?
Accepted answer
21 votes

I will give a partial answer, I hope others will fill in the blanks. In typed $\lambda$-calculi, one may give a type to usual representations of data ($\mathsf{Nat}$ for Church (unary) integers, $\...

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

At the request of Andrej and PhD, I am turning my comment into an answer, with apologies for self-advertising. I recently wrote a paper in which I look at how to prove the Cook-Levin theorem ($\...

View answer
Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?
Accepted answer
14 votes

You seem to be confusing several things here. First of all, like Alexis said in her answer, I don't see why you would need to accept/reject the principles of a given logical theory in order to study ...

View answer
Algorithm to determine function equality on the simply typed lambda calculus?
Accepted answer
14 votes

As I said in my comment, the answer in general is no. The important point to understand (I say this for Viclib, who seems to be learning about these things) is that having a programming language/set ...

View answer
Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?
Accepted answer
13 votes

First, you are confusing consistency of CIC as an equational theory with consistency of CIC as a logical theory. The first means that not all terms of CIC (of the same type) are $\beta\eta$-equivalent....

View answer
Can affine lambda calculus solve every problem in P?
Accepted answer
12 votes

Edit: my guess in the first paragraph below is wrong! Ugo Dal Lago pointed out to me a later paper by Martin Hofmann (appeared in POPL 2002), of which I was unaware, showing (as a corollary of more ...

View answer
Is there an efficient beta-equivalence algorithm?
Accepted answer
11 votes

The answer is no. An old theorem of Statman states that $\beta$-equivalence in the simply-typed $\lambda$-calculus is not elementary recursive, that is, no algorithm whose running time is bounded by $...

View answer
Why is the multi-step reduction of semantics reflexive?
Accepted answer
10 votes

The practical reason is that it is very convenient to include also the case "zero steps" in the definition of "many steps" (millennia of mathematical experience have taught us that it is usually a ...

View answer
Can Elementary Affine Logic be used as the core type system of a practical programming language?
Accepted answer
10 votes

Something very similar, but using light affine logic (LAL) instead of EAL, was attempted a few years ago by Baillot, Gaboardi and Mogbil (you may find the paper here). I think their work may be ...

View answer
Is there any known CCC closed under a probabilistic powerdomain operation?
Accepted answer
10 votes

The following is an extended comment, it does not answer your question in the terms you posed it but does give a semantics for higher-order probabilistic calculi which you may find of interest. In ...

View answer
Can you assign a type to any term of the λEA-calculus?
Accepted answer
9 votes

For question 1, the answer is no, and is no for almost any type discipline (except certain intersection types): the fact that a term is (strongly or weakly) normalizable does not imply in general that ...

View answer
What type system fits the subclass of λ-terms that can be reduced optimally?
Accepted answer
9 votes

I think that the type system you want is elementary affine logic with fixpoints. A distinctive feature (actually, the distinctive feature) of light logics, including elementary linear/affine logic, ...

View answer
What is the complexity class of higher-order primitive recursion?
Accepted answer
8 votes

If I understand correctly, the primitive recursive functionals defined in the Wikipedia page linked in the question coincide with Gödel's system T, which is well-known to correspond to the class of ...

View answer
Do we care about confluence because of unique normal forms?
Accepted answer
8 votes

I don't know what you mean by "practical", but confluence is very useful from the semantic point of view. Hopefully other people will be able to give you other answers from other points of view (for ...

View answer
Hierarchies in regular languages
8 votes

I recently came across this paper which may give another relevant example (cf. the last sentence of the abstract): Guillaume Bonfante, Florian Deloup: The genus of regular languages. From the ...

View answer
How can you encode natural numbers operations on interaction combinators?
8 votes

Contrarily to the $\lambda$-calculus, the interaction combinators have no underlying logical system (i.e., there is no Curry-Howard correspondence for them), it is therefore hard to say that a numeral ...

View answer
What are the morphisms of Adj(C,T) - the category whose objects are the adjunctions of a given monad?
Accepted answer
8 votes

The definition of morphism of adjunctions may be found in MacLane's book. Let $F:\mathcal C\rightarrow\mathcal D$, $G:\mathcal D\rightarrow\mathcal C$, $F':\mathcal C'\rightarrow\mathcal D'$, $G':\...

View answer
Are there strongly normalizing lambda terms that cannot be given a System F type?
Accepted answer
7 votes

As you found out yourself, the answer to your question is yes. You found a rather convoluted example, a much simpler example is the following: $$(\lambda zy.y(zI)(zK))(\lambda x.xx)$$ where $I$ and $...

View answer
A stronger multiplexing rule for soft linear logic?
Accepted answer
7 votes

Your rule $(\ast)$ is sometimes referred to as "absorption". I think the first who considered it was Jean-Marc Andreoli in his paper on focusing proofs. Indeed, it makes a lot of sense in proof ...

View answer
In which posets is the set of compact elements downwards closed?
Accepted answer
7 votes

The only natural condition I can think of is Berry's "I condition" ([1], Sect. 12.3): (I) each compact element dominates finitely many elements. The above condition is the defining property of Berry'...

View answer
Difference between abstract machines and calculi
Accepted answer
7 votes

I essentially agree with Martin's comment, I can elaborate on that to make a tentative answer, knowing that there is no general formal definition of calculus or abstract machine and that what I am ...

View answer
Phonology and lambda calculus
6 votes

This is just a long comment (too many words to fit in a comment box). Gérard Huet is, among other things, an expert in $\lambda$-calculus who worked worked a lot on the computational processing of ...

View answer
Calculus of Constructions: compress expression to its smallest form
6 votes

Let me insist on the viewpoint touched upon by cody's answer. As far a see it, the question of finding a smallest $\lambda$-term equivalent to another $\lambda$-term is not really interesting, even ...

View answer
Is length uniform AC0 computable?
Accepted answer
6 votes

Like Emil says, the answer is yes, because the length (in binary) of the input string is actually computable by a deterministic logtime Turing machine, so is a fortiori in $\mathsf{FO}$. You may find ...

View answer
How do you encode Lamping's abstract algorithm using interaction combinators?
Accepted answer
6 votes

I am not aware of any implementation of Lamping's algorithm directly in the interaction combinators. I do know that the presence of integer labels is a necessary feature of Lamping's algorithm, even ...

View answer
What is the relationship between intuitionistic logic, combinatory logic and lambda calculus?
Accepted answer
6 votes

I don't understand exactly what you are looking for, I'll try to explain the Curry-Howard correspondence in a nutshell, you'll let me know if it helps. The Curry-Howard correspondence (or isomorphism,...

View answer
Fixed points of fixed-point combinator?
Accepted answer
5 votes

If by "$=$" you mean $\beta$-equality, then the answer is yes, $MX=X$ for all $X$ is a stronger property than $MM=M$. For example, let $$A := \lambda a.aa(aa)$$ (to save parentheses, I am ...

View answer
How do conference proceedings add to academic prestige?
5 votes

I agree with the others that the answer to your first question is definitely "yes", and would like to add another online resource where you can have an idea of the difference in "prestige": it's the (...

View answer