Geometria interakcji

Geometria interakcji (GoI) została wprowadzona przez Jean-Yvesa Girarda wkrótce po jego pracy nad logiką liniową . W logice liniowej dowody można postrzegać jako różnego rodzaju sieci, w przeciwieństwie do płaskich struktur drzewiastych rachunku sekwencyjnego . Aby odróżnić rzeczywiste sieci dowodowe od wszystkich możliwych sieci, Girard opracował kryterium uwzględniające podróże w sieci. Wycieczki można w rzeczywistości postrzegać jako pewnego rodzaju operatora działającego na dowodzie. Opierając się na tej obserwacji, Girard opisał bezpośrednio ten operator z dowodu i podał formułę, tzw. formułę wykonania , kodującą proces eliminacji cięć na poziomie operatorów.

Jednym z pierwszych znaczących zastosowań GoI była lepsza analiza algorytmu Lampinga dla optymalnej redukcji rachunku lambda . GoI miał silny wpływ na semantykę gier dla logiki liniowej i PCF .

GoI został zastosowany do głębokiej optymalizacji kompilatora dla obliczeń lambda. Ograniczona wersja GoI, nazwana Geometry of Synthesis, została wykorzystana do kompilacji języków programowania wyższego rzędu bezpośrednio do obwodów statycznych.

Dalsza lektura

• Samouczek GoI wygłoszony w Siena 07 przez Laurenta Regniera w warsztacie Linear Logic, [2]
• Geometria interakcji w laboratorium n