Perché abbiamo bisogno di una notazione separata per i tipi П?

Aug 24 2020

Principale

Sono confuso sulla motivazione alla base della necessità di una notazione separata per i tipi П, che puoi trovare nei sistemi di tipo da λ2 in poi. La risposta di solito è così - pensa a come si può rappresentare una firma della funzione di identità - può essere λa:type.λx:a.xo λb:type.λx:b.x. La parte sottile, dicono, è che queste due firme non solo not equal, non sono equivalenti alfa come variabili di tipo ae bsono variabili libere all'interno delle loro astrazioni corrispondenti . Quindi, per superare questo fastidioso problema sintattico, presentiamo il raccoglitore П che funziona bene con la conversione alfa.

Quindi la domanda: perché è così? Perché non correggere semplicemente la nozione di equivalenza alfa?

AGGIORNAMENTO z:

Oh, sciocco da parte mia, λa:type.λx:a.xe λb:type.λx:b.xsono equivalenti alfa. Ma perché a:type -> a -> ae b:type -> b -> bnon sono allora.

AGGIORNAMENTO suc z:

Aha, interessante, immagino che questo sia un perfetto esempio di cecità selettiva =D

Sto leggendo il libro Type Theory and Formal Proof , e nel capitolo su lambda2 l'autore motiva l'esistenza Пdell'uso esattamente di quel tipo di argomentazione - non si può dire che \t:*.\v:t.v: * -> t -> tperché questo crea due termini alfa-equivalenti \t:*.\v:t.ve \g:*.\v:g.vha tipi diversi, come tipi corrispondenti non sono alfa-equivalenti, mentre i tipi simili t:* -> t -> tsono in realtà alfa-invarianti. Fai attenzione alla differenza tra t:* -> t -> te* -> t -> t . Ma non rende questo argomento un po 'banale, ed è anche qualcosa di significativo parlare di tipo a -> bin cui ae bnon sono vincolati da variabili quantificatrici. Andrej Bauersottolineato nei commenti cheПassomiglia davvero a un'astrazione lambda con alcuni campanelli e fischietti aggiuntivi.

Tutto sommato, ho finito con quello, grazie ragazzi .

Risposte

7 AndrejBauer Aug 24 2020 at 18:19

Penso che dobbiamo solo chiarire alcune cose qui:

  1. Nell'espressione$\lambda a : \mathsf{type} . \lambda x : a . x$la variabile$a$ è vincolato (dall'esterno$\lambda$). Le espressioni$\lambda a : \mathsf{type} . \lambda x : a . x$e$\lambda b : \mathsf{type} . \lambda x : b . x$ sono $\alpha$-pari.
  2. L'espressione$\lambda a : \mathsf{type} . \lambda x : a . x$ è la funzione identità, non è la "firma della funzione identità".
  3. Se per "firma della funzione identità" intendi dire "il tipo della funzione identità", allora sarebbe qualcosa di simile$\Pi_{a : \mathsf{type}} . (a \to a)$, o se vuoi solo i tipi di prodotto, allora lo è$\Pi_{a : \mathsf{type}} \Pi_{x : a} a$.

C'è ancora una domanda?

Forse questo aiuterà:

  • il tipo della funzione identità$\lambda x : a . x$è$a \to a$
  • il tipo della funzione identità$\lambda y : b . y$è$b \to b$
  • le funzioni$\lambda x : a . x$e$\lambda y : b . y$sono diversi
  • i tipi$a \to a$e$b \to b$sono diversi
  • il tipo della funzione identità polimorfica$\lambda c : \mathsf{type} . \lambda z : c . z$è$\Pi_{c : \mathsf{type}} . c \to c$.
  • le funzioni$\lambda a : \mathsf{type} . \lambda x : a . x$e$\lambda c : \mathsf{type} . \lambda z : c . z$sono$\alpha$-pari
  • i tipi$\Pi_{a : \mathsf{type}} . a \to a$e$\Pi_{c : \mathsf{type}} . c \to c$sono$\alpha$-pari.

Supplementare: dopo aver parlato con Alex Simpson davanti a una tazza di tè, c'è ancora una cosa che posso dire. Non abbiamo bisogno di separati$\lambda$e$\Pi$costruttori, poiché entrambi hanno esattamente la stessa forma sintattica (prendi due argomenti, associa una variabile). In effetti, se la mia memoria mi serve bene, Automath ha usato la stessa notazione per$\lambda$-astrazioni e$\Pi$-tipi. Ma il punto è che vogliamo usare due diversi costruttori perché denotano concetti diversi .