Strong normalization through idempotent intersection types: a new syntactical approach

1. Il Problema

Il calcolo lambda e i sistemi di tipi intersezione sono strumenti fondamentali nella teoria dei linguaggi di programmazione. È ben noto che i sistemi di assegnazione di tipi intersezione (in particolare quelli di Coppo e Dezani) possono caratterizzare la normalizzazione forte (SN): un termine $\lambda$ è tipabile se e solo se ogni sua sequenza di riduzione termina.

Tuttavia, le prove esistenti per dimostrare che i termini tipabili sono fortemente normalizzanti si basano prevalentemente su tecniche semantiche (come i candidati di riducibilità o computabilità). Sebbene valide, queste prove sono spesso considerate poco intuitive e non forniscono una misura esplicita che diminuisca ad ogni passo di riduzione.
Esistono già tre prove puramente sintattiche per la normalizzazione forte con tipi intersezione idempotenti ([22, 9, 11]), ma presentano alcune limitazioni:

• Richiedono linguaggi intermedi ad hoc o regole di riduzione non standard.
• Le misure utilizzate sono complesse (es. multi-insiemi di numeri naturali o coppie di numeri).
• Alcune approcci si basano su traduzioni verso tipi semplici che perdono informazioni, rendendo la misura meno precisa.

L'obiettivo del lavoro è fornire una nuova prova sintattica per la normalizzazione forte nel sistema di tipi intersezione idempotente, basata su una misura semplice (un singolo numero naturale) e su un approccio che operi direttamente all'interno del sistema di tipi intersezione.

2. Metodologia

Gli autori adottano un approccio strutturato in tre fasi principali, combinando la teoria dei tipi con tecniche ispirate ai calcoli della memoria (memory calculi):

A. Definizione di un Sistema Intrinsecamente Tipato ($\Lambda^i_\cap$)

Il punto di partenza è il sistema estrinseco (stile Curry) $\Lambda^e_\cap$, dove i termini sono non tipati e le regole assegnano i tipi. Per applicare la tecnica della misura decrescente, gli autori progettano una versione intrinseca (stile Church) chiamata $\Lambda^i_\cap$.

• In $\Lambda^i_\cap$, i termini sono decorati con i tipi.
• L'idea chiave è trattare l'intersezione idempotente come un insieme di tipi. Di conseguenza, la grammatica dei termini include esplicitamente insiemi di termini ($\{t_1, \dots, t_n\}$) che corrispondono a insiemi di tipi.
• Questo permette di allineare strettamente la derivazione di tipizzazione con la struttura del termine: ogni sotto-derivazione nel sistema di Curry corrisponde a un elemento distinto nell'insieme di termini nel sistema Church.

B. Integrazione con un Calcolo della Memoria ($\Lambda^{im}_\cap$)

Per gestire la riduzione in modo non cancellante (essenziale per definire una misura decrescente), gli autori introducono un calcolo ausiliario $\Lambda^{im}_\cap$.

• Questo calcolo estende $\Lambda^i_\cap$ introducendo dei wrapper (o "memorie") della forma $\langle \vec{s} \rangle$.
• Quando una riduzione $\beta$ avviene, invece di cancellare l'argomento (come nella cancellazione standard), l'argomento viene "memorizzato" in un wrapper.
• Questo trasforma ogni passo di riduzione cancellante in un passo non cancellante, preservando l'informazione necessaria per il conteggio.

C. Definizione della Misura Decrescente (Misura W)

La prova di normalizzazione forte si basa sulla definizione di una funzione $W(t)$ che associa a ogni termine un numero naturale:

1. Semplificazione Completa (Full Simplification): Si definisce un'operazione $S^*(t)$ che riduce in parallelo tutti i redex di grado massimo, poi quelli del grado successivo, fino a raggiungere la forma normale nel calcolo $\Lambda^{im}_\cap$. Questo processo è garantito dal fatto che la contrazione di un redex non può creare redex di grado superiore o uguale (osservazione di Turing).
2. Conteggio: La misura $W(t)$ è definita come il numero di wrapper presenti nel termine risultante dopo la semplificazione completa $S^*(t)$.

3. Contributi Chiave

1. Sistema $\Lambda^i_\cap$ (Church-style): Gli autori presentano una versione intrinsecamente tipata dei tipi intersezione idempotenti che simula perfettamente il sistema originale di Curry ($\Lambda^e_\cap$). Questo sistema gode di proprietà fondamentali come la riduzione del soggetto (subject reduction) e la confluenza.
2. Misura Sintattica Semplice: Viene proposta una misura di normalizzazione forte basata su un singolo numero naturale (il numero di wrapper), che è concettualmente più semplice rispetto alle misure basate su multi-insiemi o coppie utilizzate in lavori precedenti ([22, 9]).
3. Dimostrazione Diretta: A differenza di approcci che traducono i tipi intersezione in tipi semplici (perdendo informazioni), questa tecnica opera direttamente all'interno del sistema di tipi intersezione, permettendo potenzialmente analisi computazionali più fini.
4. Corrispondenza e Simulazione: Viene dimostrata la simulazione reciproca tra il sistema estrinseco $\Lambda^e_\cap$ e quello intrinseco $\Lambda^i_\cap$, garantendo che la normalizzazione forte di uno implichi quella dell'altro.

4. Risultati Principali

• Normalizzazione Forte di $\Lambda^i_\cap$: Viene provato che ogni termine tipabile in $\Lambda^i_\cap$ è fortemente normalizzante. La prova si basa sul fatto che ogni passo di riduzione $\rightarrow_i$ nel sistema intrinseco corrisponde a un passo $\rightarrow_{im}$ nel calcolo della memoria che introduce almeno un wrapper. Poiché la semplificazione completa rimuove i redex ma mantiene i wrapper, e la riduzione nel sistema intrinseco riduce il numero di wrapper necessari per rappresentare la forma normale, la misura $W(t)$ diminuisce strictamente ad ogni passo di riduzione ($W(t) > W(s)$ se $t \rightarrow_i s$).
• Caratterizzazione di $\Lambda^e_\cap$: Grazie alla simulazione, si conclude che anche il sistema originale $\Lambda^e_\cap$ (stile Curry) caratterizza esattamente la classe dei termini fortemente normalizzanti. Un termine è tipabile in $\Lambda^e_\cap$ se e solo se è fortemente normalizzante.
• Completezza: Viene dimostrato che $\Lambda^i_\cap$ (e quindi $\Lambda^e_\cap$) può tipare tutti i termini fortemente normalizzanti, confermando la potenza espressiva del sistema.

5. Significato e Implicazioni

Questo lavoro è significativo per diversi motivi:

• Chiarezza Sintattica: Fornisce una prova sintattica "pulita" per una proprietà fondamentale dei tipi intersezione, evitando l'uso di tecniche semantiche complesse e offrendo un'intuizione meccanica su perché la normalizzazione avviene (la diminuzione del numero di wrapper).
• Semplicità della Misura: L'uso di un singolo numero naturale come misura è un risultato elegante che semplifica l'analisi computazionale rispetto alle misure precedenti.
• Fondamenta per Futuri Lavori: L'approccio basato sui wrapper e sulla semplificazione completa apre la strada a ricerche future, come la definizione di una misura "esatta" (che fornisca il limite superiore esatto della lunghezza della catena di riduzione) e l'estensione di queste tecniche ad altri sistemi di tipi intersezione, ad esempio quelli che caratterizzano i termini risolvibili (solvable terms), per i quali non esistono ancora prove sintattiche di normalizzazione.

In sintesi, il paper offre un nuovo, elegante e rigoroso approccio sintattico alla normalizzazione forte nei tipi intersezione idempotenti, colmando il divario tra le prove semantiche classiche e le tecniche sintattiche moderne basate su misure decrescenti.