Domanda sul “Tutorial sull’implementazione del lambda calcolo tipizzato in modo dipendente”

Question

Ho un leggero problema tecnico con Questo meraviglioso tutorial.A pagina 5 il tutorial parla delle regole di digitazione per i Lambda Simply Typed e presenta il giudizio seguente come derivabile tramite le regole nella figura 3.

Non ho potuto dimostrare nessuno dei due id né const per lo stesso motivo.Prendiamo ad esempio il id esempio.

• Supponiamo che sto cercando una regola di controllo del tipo CHK.Dice che per check types Dovrei prima eseguire l'inferenza e poi confrontare il risultato con quello che mi aspetto.
• Per fare l'inferenza sull'applicazione, devo usare il file APP regola che mi costringe subito a dedurre la tipologia del lato sinistro della domanda, vale a dire (id :: α -> α)
• Per farlo sto utilizzando il file ANN regola che mi obbliga a verificarlo α -> α è un tipo (e posso dimostrarlo senza problemi).Poi l'ho messo nudo id simbolo e devo dimostrare che è il tipo α -> α.
• Infine, ecco un problema.Per fare ciò dovrò usare var regola, che richiede il tipo di id da impostare esplicitamente nel contesto Gamma, ma non viene fatto, quindi la dimostrazione sta cadendo a pezzi.

Answer 1

$\mathsf{id}$ E $\mathsf{const}$ non sono variabili del calcolo, ma zucchero sintattico per $\lambda x ightarrow x$ E $\lambda x ightarrow \lambda y ightarrow x$ rispettivamente.Ciò è affermato alla fine del §2.2 e sottilmente trasmesso dall'uso di un carattere sans-serif anziché il corsivo (si tratta di una convenzione tipografica di questo particolare documento, non di una convenzione comune).

Quindi, ad esempio, il giudizio sul tipo$$ Alpha ::\ast, y ::\alpha \vdash (\mathsf{id} ::\alpha ightarrow \alpha) \:sì ::Rightarrow alpha $$è anche il giudizio di tipo$$ Alpha ::\ast, y ::\alpha \vdash (\lambda x ightarrow x ::\alpha ightarrow \alpha) \:sì ::Rightarrow Alpha.$$È una notazione diversa per lo stesso oggetto matematico.