3
$\begingroup$

I wonder if there is some direct proof of how $\lambda$-$\mu$-calculus maps to classical logic via the Curry-Howard correspondence. Just like one can verify a valid sentence in propositional logic by stupidly checking truth tables, I'm curious if there is a similarily stupid (not necessarily efficient!) algorithm to find a $\lambda$-$\mu$-term belonging to a given (classically valid) type.

I imagine some kind of dialogue game, I try to prove $P:=P_0\Rightarrow P_1$, either there is already an intuitionistic proof, in which case I'm done. Otherwise, I pretend to have a term of type $P$ and see if my opponent feeds something of type $P_0$ into it. I continue recursively and every time I encounter an atom, then somehow return it to the root (this part I'm not sure how to do in $\lambda$-$\mu$-calculus).

Let $X$ be the subset of atoms in $P$ which evaluate to true (in a given interpretation), $P_1$ is then either classically true or false. In the first case, I assume to get enough ressources while recursively poking $P_0$ so that I can continue at the root and construct $P_1$. In the other case, my bluff of calling $P$ is never revealed.

Is there some way to formalize this idea in $\lambda$-$\mu$-calculus?

$\endgroup$

1 Answer 1

2
+100
$\begingroup$

What you are referring to is called the type inhabitation problem. Since for the simplest case, simply typed $\lambda$-calculus, the problem is PSPACE complete, any generalization of that inherits this difficulty.

UPDATE: (To account for the comments)

One can extract the term that inhabits the given type using prover skeptic dialogues. You may search further, and I would recommend reading about the simpler case of intuitionistic formulae with implication symbol only.

Your analogy with brute-force checking the truth tables of a formula does not stand. Lambda terms are a formality for describing proofs, and propositional formulae are to be proven. Brute forcing the truth tables outputs yes or no, where inhabitation of a type provides a formal proof. The first being on the semantics side, the other on the syntax side.

$\endgroup$
5
  • $\begingroup$ OK, but truth tables checking is exponential in complexity (I think?), so what is the implication? $\endgroup$
    – fweth
    Oct 11, 2022 at 8:17
  • $\begingroup$ Just that it is difficult to even find resources on the subject. Also, if we naively think about it, type inhabitation is like searching for a formal proof of the given formula. This by the CHC. It is definitely not something that is easily computed. $\endgroup$
    – Jason
    Oct 11, 2022 at 8:23
  • $\begingroup$ Yes, but I'm not looking for an effective computation, just for a stupid one. BTW I didn't give you the downvote! $\endgroup$
    – fweth
    Oct 11, 2022 at 8:25
  • $\begingroup$ I have deleted my last comment and updated my answer. $\endgroup$
    – Jason
    Oct 13, 2022 at 6:17
  • $\begingroup$ Cool, thanks! I'll accept the answer later but I just want to leave it open for a few days to see if somebody else comments... Do you maybe have an example of a $\lambda$-$\mu$-term of type $P\to Q$ where $Q$ is not an atom? $\endgroup$
    – fweth
    Oct 13, 2022 at 6:29

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .