Zastosowania geometrii algebraicznej w teorii typów / teorii języka programowania

Ostatnio zainteresowałem się geometrią algebraiczną i zacząłem o niej czytać. Wciąż bardzo mało wiem o tym polu, ale chcę wiedzieć, czy ma on jakiś związek z moim głównym polem, teorią typów i językami programowania.

Wiem, że topologia algebraiczna ma wiele zastosowań w teorii typów (teoria homotopii i wiele innych), ale co z geometrią algebraiczną, poza tym, że zarówno teoria typów / teoria PL, jak i AG są dobrymi motywatorami teorii kategorii?

Według mojej wiedzy (która jest zdecydowanie niekompletna) prace nad tym były stosunkowo niewielkie, prawdopodobnie dlatego, że wymagają one przyswojenia dwóch względnie skomplikowanych zasobów wiedzy. Jednak niewiele nie oznacza nieistnienia. Thierry Coquand i jego współpracownicy napisali sporo artykułów na temat powiązań między algebrą przemienną a konstruktywną logiką.

• Thierry Coquand, Henri Lombardi. Logiczne podejście do algebry abstrakcyjnej .

  Ten artykuł wywarł na mnie ogromne wrażenie jako student - pewny siebie i swobodny sposób, w jaki wykorzystywał pomysły z teorii dowodów i teorii modeli do robienia nietrywialnej, właściwej matematyki, którą bardzo podziwiałem i do której wciąż dążę.

• Henri Lombardi i Claude Quitté mają (ogólnodostępny) podręcznik Algebra komutacyjna: metody konstruktywne .

  Jak sugeruje tytuł, jest to algebra komutatywna, a nie geometria algebraiczna, ale ponieważ algebra komutacyjna zapewnia znaczną część infrastruktury dla geometrii algebraicznej, nadal będzie to interesujące.

Istnieje również wiele bardzo ciekawych prac doktorskich w tej dziedzinie:

• Praca doktorska Andresa Mörtberga Formalizowanie udoskonaleń i algebry konstruktywnej w teorii typów

  Gdy masz konstruktywny dowód, masz algorytm. Ta teza dotyczy sprawnego działania tych algorytmów.

• Praca doktorska Bassela Mannai, Semantyka snopa w algebrze konstrukcyjnej i teoria typów

  W tej pracy konstruktywnie dowodzi poprawności twierdzenia Newtona-Puiseuxa, a także niezależności zasady Markowa. To dobry przykład tego, w jaki sposób metody sheaf-semantyczne mają zastosowanie zarówno w geometrii, jak i logice.

• Rozprawa doktorska Ingo Blechschmidta, Używając wewnętrznego języka toposów w geometrii algebraicznej,

  Teza ta dotyczy powtórzenia wielu zwykłych dowodów geometrii algebraicznej w języku wewnętrznym małych toposów Zariski związanych ze schematem, dając rodzaj „syntetycznej geometrii algebraicznej”. (Robi także „teorię schematu syntetycznego”, używając dużych toposów Zariski). Jak można się spodziewać, ponieważ topoi nie są na ogół logiczne, dowody muszą być wykonane w intuicyjnym stylu.

Warto również zwrócić uwagę na następujące odniesienie:

• Saunders Mac Lane, Ieke Moerdijk. Krążki w geometrii i logice Krążki w geometrii i logice: Pierwsze wprowadzenie do teorii toposu .

  Wiele technologii wykorzystywanych w tej pracy pochodzi z połączeń teorii toposu, logiki i geometrii. Jest to standardowe odniesienie, chociaż nauczyłem się go głównie dzięki pracom Steve'a Vickersa.

Być może nie jest to dokładnie to, czego szukasz, ale jednym z zastosowań geometrii algebraicznej w językach programowania jest analiza pętli liniowych:

Pętla liniowa jest bardzo prostym programem o postaci:

$x=s$

Podczas $x\notin F$

$x\leftarrow Ax$

Gdzie $s,x\in \mathbb Q^d$ i $A\in \mathbb Q^{d\times d}$jest matrycą. Zestaw$F$ to warunek kończący, którym może być jakiś prosty zestaw (np. zestaw politopowy lub zestaw semialgebraiczny).

Analiza tych pętli często sprowadza się do analizy orbity macierzy$A$, mianowicie $\{A^ns: n\in \mathbb N\}$. To z kolei wiąże się z analizą potęg wartości własnych$A$, którego zachowanie ma ścisły związek z pojęciami w geometrii algebraicznej (np. podstawowe twierdzenie Massera).

Dobrym punktem wyjścia może być artykuł o złożoności problemu orbity .