Pytania otagowane jako parametricity

4
Jakie są różnice między relacjami logicznymi a symulacjami?
Jestem początkującym pracującym nad metodami potwierdzającymi równoważność programu. Przeczytałem kilka artykułów na temat definiowania relacji logicznych lub symulacji, aby udowodnić, że dwa programy są równoważne. Ale jestem dość zdezorientowany co do tych dwóch technik. Wiem tylko, że relacje logiczne są definiowane indukcyjnie, podczas gdy symulacje oparte są na koindukcji. Dlaczego …
4
Jedność parametryczna a parametryczność binarna
Ostatnio zainteresowałem się parametrownością po obejrzeniu artykułu LICS Bernardy'ego i Moulina z 2012 r. ( Https://dl.acm.org/citation.cfm?id=2359499 ). W tym artykule internalizują one jednoargumentową parametryczność w systemie czystego typu z typami zależnymi i podpowiadają, w jaki sposób można rozszerzyć konstrukcję na dowolne arie. Wcześniej widziałem tylko parametr binarny. Moje pytanie brzmi: …
3
Jak można motywować relacyjną parametryczność?
Czy istnieje jakiś naturalny sposób na zrozumienie istoty semantyki relacyjnej polimorfizmu parametrycznego? Właśnie zacząłem czytać o pojęciu parametryczności relacyjnej, a la John Reynolds „Typy, abstrakcja i polimorfizm parametryczny” i mam problem ze zrozumieniem, w jaki sposób motywowana jest semantyka relacyjna. Zestaw semantyki ma dla mnie idealny sens i zdaję sobie …
1
Dlaczego wykresy refleksyjne dla parametryczności?
Patrząc na modele polimorfizmu parametrycznego, jestem ciekawy, dlaczego stosowane są kategorie wykresów refleksyjnych ? W szczególności dlaczego nie zawierają składu relacyjnego? Patrząc na modele, wszystkie wydają się potwierdzać naturalne pojęcie składu relacyjnego: x(R;S)z⟺∃y.xRy∧ySzx(R;S)z⟺∃y.xRy∧ySz x(R;S)z \iff \exists y. xRy \wedge y S z Najnowsze artykuły, które używają wykresów refleksyjnych, wydają się …
1
Naturalne transformacje i parametryczność
W twierdzeniach za darmo! , Wadler mówi, że charakterystykę parametryczności można wyrazić ponownie w kategoriach luźnych naturalnych przekształceń i będzie to przedmiotem kolejnego artykułu. Do którego referatu się odnosi? W znanym mi kategorycznie podejściu do paramteryczności stosuje się transformacje dinaturalne, jak w polimorfizmie funkcjonalnym Bainbridge, Freyda, Scedrowa i PJ Scotta. …
1
Gdzie badana jest parametryczna relacja w modelach hiperdoktryny lub toposu?
Reynolds pierwotnie zaproponował semantykę relacyjną dla polimorficznego rachunku lambda drugiego rzędu [1]. Później jednak wykazał [2], że to podejście było niespójne z klasyczną teorią zbiorów. Pitts opisał ramy modeli hiperdoktryn i modeli topos [3], które są spójne z logiką konstruktywną. Następnie opracowano przypuszczalnie relacyjne modele hiperdoktryny i toposu. Gdzie mogę …
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.