1
$\begingroup$

In Definition 3.2 (page 12) of Gallier's 'Constructive Logics Part I: A Tutorial on Proof Systems and Typed Lambda-Calculi' he sets out the rules for his typed $\lambda^{\to, +, \times, \perp}$-calculus. I've studied simply typed $\lambda$-calculus before so understand most of what he's saying, however was unsure about a few bits of notation, and couldn't find a definition (or intended interpretation) anywhere in the text/online. (I've switched Gallier's $\rhd$ for $\vdash$ as it's what I'm more used to.)

  1. First in $\perp$-elim, the use of $\nabla$: $$\frac{\Gamma \vdash M:\perp}{\Gamma \vdash \nabla_A(M): A}$$

  2. Then in the 'by cases' rule, the use of $\texttt{case}$: $$\frac{\Gamma \vdash P : A + B \quad \Gamma, x:A \vdash M : C \quad \Gamma, y : B \vdash N : C} {\Gamma \vdash \texttt{case}(P, \lambda x: A.M, \lambda y: B.N) : C}$$

Any help/clarification appreciated.

$\endgroup$
1
  • $\begingroup$ No hint in the Lecture of what the "inverted Delta"(M) means? $\endgroup$ Dec 23, 2021 at 14:34

1 Answer 1

5
$\begingroup$

These are the definitions of $\nabla_A$ and $\texttt{case}$. These are freely defined constructors of type $$\nabla_A : \bot\to A$$ and $$\texttt{case} : A + B\to (A\to C) \to (B \to C) \to C.$$ They don't reduce to anything. They are simply the proof constructors corresponding to elimination of $\bot$ and $+$.

$\endgroup$

You must log in to answer this question.

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