Czy potrafisz wyjaśnić intuicję stojącą za spójnymi przestrzeniami?

Logika liniowa jest interpretowana za pomocą Spójnych przestrzeni i są one wyraźnie widoczne w artykułach Girarda. Znam wszystkie trzy główne sposoby formalnego ich zdefiniowania i tak naprawdę nie stanowią żadnego problemu w używaniu i udowadnianiu różnych rzeczy, ale po prostu nie rozumiem, co one oznaczają .

Naprawdę wydaje się, że istnieje jakiś sposób na ich zrozumienie . Przede wszystkim jest kilka przykładów na ich temat, które używają funkcji na boolach (jak gdzieś na wiki ). I wskazuje na coś interesującego i znaczącego za formalną definicją. Jednakże, booljest to bardzo proste, spójne przestrzeń, bez kliki rozmiaru > 1. Czy ktoś może opracować?

Kolejna rzecz, Girard mówi gdzieś, że każdy punkt spójnej przestrzeni reprezentuje określoną „sekwencję pytań / odpowiedzi”, przy czym dwa punkty są spójne, jeśli „rozwidlają się negatywnie (tj. W przypadku różnych pytań)”, i niespójne, jeśli dzielą się na różne odpowiedzi [1] Wydaje się, że to prosty pomysł, ale po prostu nie mogę wymyślić żadnego przykładu, więc oznacza to, że tak naprawdę go nie rozumiem ...

Czy ktoś mógłby mi w tym pomóc?

[1] JY Girard, Upiór przejrzystości . URL: http://iml.univ-mrs.fr/~girard/longo1.pdf

Intuicja stojąca za przestrzeniami koherencji jest taka, że ​​elementy przestrzeni koherencji reprezentują obserwacje niektórych podstawowych danych, a relacja koherencji mówi ci, czy dwie obserwacje mogły pochodzić z tego samego fragmentu danych.

Konkretnie, załóżmy, że mamy zestaw zwierząt

Animals = {cat, duck, fish}

Teraz możemy mieć zestaw obserwacji:

Observations = {warm-blooded, swims, water-breathing, furry}

Powiedzmy, że dwie obserwacje są kompatybilne, jeśli mogłyby być wykonane z tego samego zwierzęcia. Każda obserwacja jest zgodna z samym sobą, a ponadto:

• $\stackrel{{\large\frown}}{{\small\smile}}$
• $\stackrel{{\large\frown}}{{\small\smile}}$
• $\stackrel{{\large\frown}}{{\small\smile}}$
• $\stackrel{{\large\frown}}{{\small\smile}}$

Wiemy, że ciepłokrwistość jest zgodna z pływaniem, ponieważ kaczki są ciepłokrwiste i pływają. Ale bycie ciepłokrwistym i oddychanie wodą nie są kompatybilne, ponieważ nie mamy zwierząt, które są ciepłokrwiste i oddychają wodą.

Observations$\stackrel{{\large\frown}}{{\small\smile}}$Observations$\stackrel{{\large\frown}}{{\small\smile}}$

Zawsze miałem problem z tworzeniem intuicji dla przestrzeni koherencyjnych, dopóki nie zapoznałem się z teorią domen i przeczytałem Girarda „System F typów zmiennych, piętnaście lat później”. Przestrzenie koherencji są tylko specjalnym rodzajem domeny i znacznie łatwiej było mi zrozumieć, co oznacza koherencja od tego miejsca. Spróbuję podać wyjaśnienie, które miało dla mnie mniej więcej sens.

Wyobraź sobie, że chcesz studiować programy, które przyjmują liczby całkowite do liczb całkowitych. Ogólnie rzecz biorąc, programy te mogą zapętlać się w nieskończoność, więc sensowne jest modelowanie ich matematycznie jako funkcje cząstkowe od liczb całkowitych do liczb całkowitych: jeśli program zapętla się, odpowiednia funkcja częściowa jest niezdefiniowana na tym wejściu. Taką funkcję cząstkową możemy wyświetlić fjako wykres : zestaw par liczb całkowitych (n, m)takich, które fsą zdefiniowane ni równe m. Pozwala nam to przedstawić te funkcje jako przestrzeń koherencji:

• Sieć przestrzeni koherencji jest zbiorem par liczb całkowitych (n, m).
• Dwie pary (n, m)i (n', m')są spójne tylko wtedy, gdy ni n'są różne, albo mi m'są równe.

Po rozpakowaniu definicji widzimy, że każda klika tej przestrzeni koherencji jest wykresem funkcji cząstkowych i odwrotnie. Możemy interpretować relację koherencji jako powiedzenie, że jeśli jedna funkcja cząstkowa jest zdefiniowana na wejściu, to daje tylko jeden wynik dla tego wejścia. Jeśli jesteś przyzwyczajony do innych rodzajów semantyki teoretycznej, włączenie klików odpowiada zwykłemu porządkowi Scotta w zakresie funkcji cząstkowych na liczbach całkowitych.