0
$\begingroup$

I am trying to translate the following definition (in Agda) of intrinsically scoped terms of the untyped lambda calculus into more mathematical (in particular set theoretical) notation:

data _⊢_ : Context → Type → Set where

  `_ : ∀ {Γ}
    → Γ ∋ ★
      -----
    → Γ ⊢ ★

  ƛ_  :  ∀ {Γ}
    → Γ , ★ ⊢ ★
      ---------
    → Γ ⊢ ★

  _·_ : ∀ {Γ}
    → Γ ⊢ ★
    → Γ ⊢ ★
      ------
    → Γ ⊢ ★

Variables are represented by De Bruijn indices.

This is my current attempt:

The set of terms in context $\Gamma$ (which is just a natural number) is denoted by $\Lambda(\Gamma)$ and is inductively generated by the following functions:

  • $\textsf{var}_\Gamma : \{1, \dots, \Gamma\} \to \Lambda(\Gamma)$
  • $\textsf{abs}_\Gamma : \Lambda(\Gamma + 1) \to \Lambda(\Gamma)$
  • $\textsf{app}_\Gamma : \Lambda(\Gamma) \times \Lambda(\Gamma) \to \Lambda(\Gamma)$

I am not happy with this attempt. Here are my thoughts:

  • I know that for each $\Gamma$, the set $\Lambda(\Gamma)$ contains infinitely many terms, but still it seems to be wrong to define each $\Lambda(\Gamma)$ in terms of a still undefined set $\Lambda(\Gamma + 1)$. See $\textsf{abs}_\Gamma$.
  • It feels strange to only write down the function signatures without saying what the functions are actually "doing". I could say that $\{1, \dots, \Gamma\} \subseteq \Lambda(\Gamma)$ and that $\textsf{var}_\Gamma$ is the inclusion map, but this would only solve a part of the problem, I think.

If someone could help me with this, it would be much appreciated.

$\endgroup$
2
  • $\begingroup$ > It feels strange to only write down the function signatures without saying what the functions are actually "doing". Do you mean a 'data constructor'? $\endgroup$ Apr 16 at 10:48
  • $\begingroup$ Yes, I'm talking about the constructors. I know that they just construct the elements of the set of terms, so what they "do" is encoded in the signatures. In set theoretic terms there is a distinction though between a function signature and its definition, isn't it? $\endgroup$ Apr 16 at 11:01

0

You must log in to answer this question.