Klop, van Oostrom i de Vrijer mają papier na rachunku lambda z wzorami.
http://www.sciencedirect.com/science/article/pii/S0304397508000571
W pewnym sensie wzór jest drzewem zmiennych - choć myślę o nim jako o zagnieżdżonej krotce zmiennych, na przykład ((x, y), z), (t, s)).
W artykule wykazali, że jeśli wzory są liniowe, w tym sensie, że żadna zmienna we wzorze nie jest powtarzana, wówczas obowiązuje reguła
(\p . m) n = m [n/p]
gdzie p jest zmiennym wzorem, a n jest krotką terminów o dokładnie takim samym kształcie jak p, jest zbieżny.
Jestem ciekawy, czy w literaturze istnieją podobne zmiany dotyczące rachunku lambda z wzorami i dodatkową zasadą eta (ekspansja, redukcja lub po prostu równość).
W szczególności chodzi mi o eta
m = \lambda p . m p
Mówiąc wprost, jestem ciekawy, jakie właściwości miałby taki rachunek lambda. Na przykład czy jest zbieżny?
Wymusza zamknięcie kategorii klasyfikacyjnej, ponieważ wymusza to właściwość
m p = n p implies m = n
Korzystając z reguły \ xi pomiędzy. Ale może coś może pójść nie tak?
źródło
Odpowiedzi:
To nie jest pełna odpowiedź; jest to komentarz, który stał się zbyt duży.
Jeśli rozszerzysz typowany rachunek lambda o produkty z eliminatorami projekcyjnymi (tj. Eliminatorami produktów
fst(e)
isnd(e)
), nie ma zasadniczo żadnych problemów. Powodem, dla którego zajęło to tak dużo czasu, jest to, że okazuje się, że bardziej naturalne jest tworzenie rozszerzeń eta niż zmniejszanie eta . Zobacz Barry Jay's The Virtues of Eta Expansion .Jeśli chcesz, aby produkty miały eliminator wzorowany na wzorach
Wtedy sprawy są bardziej złożone. Podstawową trudnością związaną z dopasowaniem wzorca są konwersje dojazdów do pracy . Oznacza to, że rachunek różniczkowy ma równanie
i zastanawianie się (a), którego kontekstu
C[-]
użyć i (b) jak zorientować to równanie, staje się trudne. IMO, najnowocześniejszym podejściem do stylów przepisywania jest Extrafing Recriting with Sums Sama Lindleya i Decydent Equivalence with Sums Gabriela Scherera i objaśnianie pustego typu , przy czym oba uwzględniają zapisany rachunek lambda zarówno z produktami, jak i sumami.źródło