Call-by-push-value - Call-by-push-value

W programowaniu teorii języka The call-by-push-wartość ( CBPV ) paradygmat, zainspirowany monad , umożliwia pisanie semantyki dla lambda-rachunek bez pisania dwa warianty do czynienia z różnicą pomiędzy call-by-name i call-by-value . W tym celu CBPV wprowadza termin język rozróżniający obliczenia i wartości, zgodnie ze sloganem wartość jest, obliczenie robi ; ten termin język ma jedną kolejność oceny. Jednakże, aby ocenić termin rachunku lambda zgodnie ze strategią redukcji call-by-name ( CBN ) lub call-by-value ( CBV ) , można przetłumaczyć ten termin na CBPV za pomocą call-by-name lub call- strategia tłumaczenia według wartości, które powodują powstanie różnych terminów. Ocena wyniku tłumaczenia call-by-value odpowiada ocenie oryginalnego terminu za pomocą strategii call-by-value; ocena wyniku tłumaczenia call-by-name odpowiada zamiast tego ocenie oryginalnego terminu za pomocą strategii call-by-name.

Jest to szczególnie przydatne, gdy mamy do czynienia z semantyką różnych skutków ubocznych, takich jak brak terminacji, stan zmienny lub niedeterminizm. Zamiast podawać dwa warianty semantyki, jeden dla kolejności oceny call-by-name i jeden dla call-by-value, można po prostu podać semantykę dla języka terminów CBPV; otrzymujemy dwie semantyki dla rachunku lambda, składając semantykę CBPV z tymi samymi tłumaczeniami CBV i CBN z rachunku lambda.

Bibliografia