Rozszerzenie Eta we wzorze rachunku lambda

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?

— Jonathan Gallagher
źródło

Czy potrafisz napisać put, co masz na myśli mówiąc o eta? O ile nie jest to bardzo dziwne, powinieneś być w stanie zakodować go za pomocą sum i wykonać argument symulacyjny.

— Maks. Nowy

@ MaxNew: wygląda na to, że pyta o nietypowy rachunek różniczkowy. Wszystko o wzorach działa idealnie z typami (och, tak skromnie sugeruję własne skupienie się na dopasowywaniu wzorców ), ale nieoparty rachunek lambda różni się wystarczająco od wpisanego LC (szczególnie wrt eta), że nie odważę się odpowiedzieć bez wykonania dowodów .

— Neel Krishnaswami

@MaxNew: Co pociąga za sobą kodowanie sumami?

— Jonathan Gallagher

@NeelKrishnaswami: Tak naprawdę interesuje mnie jedno i drugie. Myślę, że denerwuję się posiadaniem zmiennych typu produktu wraz z regułą eta. Myślę, że tak się dzieje, na przykład dicosmo.org/Articles/JFP96.pdf . Ale jeśli się mylę, popraw mnie. Masz wtedy równości takie jak \ lambda x .mx = m = \ lambda (p, q). m (p, q), na przykład. Dziękuję za link do twojego artykułu!

— Jonathan Gallagher

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)i snd(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

let (a,b) = e in t

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

C[let (a,b) = e in t] === let (a,b) = e in C[t]

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.

— Neel Krishnaswami
źródło