Damiano Mazza
• Member for 8 years, 1 month
• Last seen more than a week ago
• Paris, France

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 ...

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 ...

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 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 ($\...

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 ...

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 ...

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....

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 ...

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 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 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 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 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 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 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 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 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 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 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':\...

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 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 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 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 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 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 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 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 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 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 ...