Questions tagged [lambda-calculus]

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

Filter by
Sorted by
Tagged with
0 votes
3 answers

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 ...
user avatar
4 votes
1 answer

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 ...
aradarbel10's user avatar
1 vote
0 answers

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 ...
Alex Byard's user avatar
5 votes
1 answer

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 ...
Gabriele Cecilia's user avatar
3 votes
1 answer

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 ...
tinlyx's user avatar
  • 1,906
1 vote
1 answer

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 ...
Daniel Donnelly's user avatar
1 vote
1 answer

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 ...
tryst with freedom's user avatar
10 votes
2 answers

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 ...
Itai Zukerman's user avatar
19 votes
1 answer

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 ...
Couchy's user avatar
  • 2,181
9 votes
2 answers

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 ...
sparusaurata's user avatar
9 votes
3 answers

Generic proof assistants/modularity of the proof assistants?

One notable feature of Isabelle is that it allows for the definition and in-built integrated support of alternative object logics via the interface of Isabelle/Pure in combination with Isabelle/Isar. ...
user9716869 - supports Ukraine's user avatar
10 votes
3 answers

Is there something special about weak head normal form used with proof assistants?

Is there something special about weak head normal form used with proof assistants? What I am seeking does not have to be specific just something to act like a compass to give me an indication of what ...
Guy Coder's user avatar
  • 2,836