Questions tagged [lambda-calculus]

Use this tag when asking a question that is not about a specific Lambda-calculus such as pure, typed, etc.

13 questions
Filter by
Sorted by
Tagged with
1 vote
129 views

What is the $\mu$ in the labmda calculus defined here?

In the Lambda: Introduction to Lambda Calculus chapter of PLFA, it has the following definition for the lambda calculus, which includes a $\mu$ operator that I haven't seen before. Syntax of terms ...
• 2,220
461 views

LEM, the halting problem, the curry-howard correspondence -> deep connection?

I posted the following on the math stackexchange, but it occurs to me that this might be a more (or at least equally?) appropriate forum: It was recently said to me by a prominent mathematician, who I ...
121 views

How to encode and manipulate (parallel) substitutions?

While attempting to formalize some basic properties of STLC I fell into a very deep rabbit hole revolving around substitutions. Apparently there are a few different ways to go about it, including ...
• 319
1 vote
67 views

Can you help me lay out the different variations of CoC and their generalizations?

I am learning the typed lambda-calculus and looking into the Calculus of Constructions. It was going well until I was slapped in the face with variations, and now I'm confused about the layout of all ...
• 486
123 views

Is there any formalization (with any theorem prover) of the Bohm theorem for lambda-calculus?

I am an university student working on a thesis about λ-calculus. I'd like to know if there's any article or publication about proof assistant formalizations of the Bohm theorem ("any two normal ...
156 views

untyped lambda expressions may not have normal forms; are they used (or OK to use) in proof assistants?

I heard that untyped lambda expressions can have no normal forms. As an example, the expression $(\lambda x. x\space x) (\lambda x. x\space x)$ , when put to a $\beta$ conversion, gives back the same ...
• 2,220
1 vote
556 views

How does Lean4 (or a typical PA) represent lambda functions or in other words arbitrary expressions?

Question: Say I wanted my language to support various operator symbols, the semantics of which are defined by the user or by axioms. I'm wondering whether Lean4 (or a typical well-known PA) just ...
1 vote
125 views

Natural deduction vs simply typed lambda calculus

In ND , I have propositions as their own things, but in simply typed lambda calculus, I have propositions associated with proof. The question I want to ask is, how do these two different way of ...
1k views

Constructive proof of strong normalization for simply typed lambda calculus

I'm reading Girard's Proofs and Types, and in section 4.4 he writes: Lemma: t is strongly normalisable iff there is a number ...
1k views

When should I use De Bruijn levels instead of indices?

I am familiar with De Bruijn indices, but not with De Bruijn levels. In my understanding, indices index variables from the top of the context/stack, whereas levels index variables from the bottom. So ...
• 2,300
453 views

Comparison between proof assistants for coinductive structures and proofs

I have a quite vague and naïve question: what are the differences between the different proof assistants regarding coinduction? My motivation is that I'd like to formalize some proofs, basically about ...
• 229