Gruppo di Logica e Geometria della Cognizione

Ehrhard e Regnier hanno definito l'espansione di Taylor di un lambda-termine ordinario come una combinazione lineare infinita di termini del lambda-calcolo con risorse. Il lambda-calcolo con risorse è una variante del lambda-calcolo ordinario in cui invece dell'applicazione ordinaria è presente un'applicazione "lineare". A livello logico, il lambda-calcolo con risorse corrisponde alle reti differenziali senza la promozione. Servendosi di una proprietà di uniformità, Ehrhard e Regnier hanno mostrato che la somma delle forme normali dei termini che compaiono nell'espansione di Taylor di un lambda-termine ordinario M è l'espansione di Taylor dell'albero di Böhm di M. Presenteremo brevemente tali risultati e uno degli attuali obiettivi di ricerca (ancora in fieri): caratterizzare la proprietà di uniformità nelle reti differenziali senza promozione.