Rachunek Lambda: różnica między kontekstami a kontekstami oceny

Po pierwsze, chciałbym powiedzieć, że mój tekst poniżej może zawierać błędy, więc możesz wskazać wszelkie błędy w moim sformułowaniu pytania.

Rozważ niepoprawny rachunek lambda z wartościami logicznymi i instrukcjami if, których warunki są podane przez tę składnię:

 t ::= v | t t | if t t t | x
 v ::= \x.t | #t | #f

Konteksty C w tym przypadku byłyby podane zgodnie z następującą składnią:

C ::= [-] | \x. C | C t | t C | if C t t | if t C t | if t t C

Dodatkowo można zdefiniować konteksty oceny E zgodnie z inną składnią:

E ::= [-] | \x. E | v E | E t | if E t t

Podzieliłem moje pytanie na trzy podpunkty, którymi chciałbym się zająć.

Kiedy stosuje się te dwa pojęcia? Wiem na przykład, że konteksty oceny są używane do definiowania semantyki rachunku różniczkowego, ale użycie kontekstów wciąż mi umyka. Chciałbym też trochę potwierdzić moją wiedzę tutaj.
Kiedy należy preferować jedno i dlaczego?
Czy możesz wskazać odpowiednie artykuły, które mogą pomóc mi w rozwiązaniu tej kwestii?

programming-languages lambda-calculus

Kontekst jest wykorzystywany do wielu celów, ale zwykle do definiowania zgodności programów. Konteksty oceny są podzbiorem kontekstów. Są zwykle używane do definiowania relacji redukcji. Podam przykład każdego z nich.

Jednym z formalnych sposobów definiowania równości programu jest stwierdzenie, że dwa programy i są kontekstowo równe i mogą się wzajemnie zastępować w każdym kontekście bez zmiany zachowania. Można to określić w następujący sposób: i są kontekstowo równe dostępne dla wszystkich sytuacjach końcowych o i : tylko wtedy, gdy . Mówimy, że dla kontekst się kończy $M$ $N$ $M$ $N$ $C[\cdot]$ $M$ $N$ $C[M] \Downarrow t$ $C[N] \Downarrow t$ $M, N$ jeśli ani ani mają wolnych zmiennych. EXPRESSION oznacza, że program zmniejsza się skończoną liczbę kroków do wartości . (Nawiasem mówiąc, należy zauważyć, że definicja równoważności kontekstowej jest bardziej zaangażowana w przypadku bogatych pojęć obliczeniowych, np. Równoległych procesów). $C[M]$ $C[N]$ $M \Downarrow t$ $M$ $t$

\frac{M \to N}{E [M] \to E [N]}

$\frac{M \rightarrow N}{E[M] \rightarrow E[N]}$

λ

$\lambda$

λ

$\lambda$

M \to N

$M \rightarrow N$

λ x . M \to λ x . N

$\lambda x.M \rightarrow \lambda x.N$

λ

$\lambda$ Zrewidowany raport na temat syntaktycznych teorii kontroli sekwencyjnej i stanu autorstwa Felleisen i Hieb.

— Martin Berger
źródło

$[]$

C ::= [] ∣ x ∣ t C ∣ C t ∣ λ x . C

$C ::= [] \mid x \mid t \, C \mid C \, t \mid \lambda x.C$

$C[]$ $t$ $C[t]$ $t$ $[]$ $C[t]$ $[]$ $t$

(λ x . M) N \to_{β} M {x \leftarrow N}

$(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}$

M {x \leftarrow N}

$M \{x\leftarrow N\}$

x \mapsto N

$x \mapsto N$

M

$M$

$t$ $M$ $N$ $x$ $t = (\lambda x. M) \, N$ $t$ $t'$ $t' = (\lambda x. M) \, N$ $t$ $C$ $M$ $N$ $x$ $t = C[(\lambda x. M) \, N]$ $C[M \{x\leftarrow N\}]$

\frac{}{(λ x . M) N \to_{β} M {x \leftarrow N}} (β) \frac{M \to_{β} N}{C [M] \to_{β} C [N]} (γ)

$\dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \qquad \dfrac{M \to_\beta N}{C[M] \to_\beta C[N]} (\gamma)$

\frac{}{(λ x . M) N \to_{β} M {x \leftarrow N}} (β) \frac{M \to_{β} N}{λ x . M \to_{β} λ x . N} (C_{λ}) \frac{M \to_{β} N}{M P \to_{β} N P} (C_{@ <}) \frac{M \to_{β} N}{P M \to_{β} P N} (C_{@ >})

$\dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_\beta N}{\lambda x. M \to_\beta \lambda x. N} (C_\lambda) \qquad \dfrac{M \to_\beta N}{M \, P \to_\beta N \, P} (C_{@\lt}) \qquad \dfrac{M \to_\beta N}{P \, M \to_\beta P \, N} (C_{@\gt})$

Ta definicja daje redukcję beta, tzn. Pojęcie oceny, które pozwala na ograniczenie dowolnego okresu. Obliczenia wykonywane w językach programowania często nie pozwalają na ograniczenie subtermów w funkcjach: reguła redukcji może być zastosowana tylko na najwyższym poziomie, lub po lewej lub prawej stronie aplikacji. Możemy to wyrazić, definiując nowy rodzaj kontekstu, który nie zezwala na wszystkie formy składniowe: Możemy użyć tej składni do zdefiniowania pojęcia semantycznego bez oceny częściowej: Możemy również przedstawić tę definicję, rozszerzając ją, tak jak to zrobiliśmy powyżej dla pełnej redukcji wersji beta:

D ::= [] ∣ x ∣ t D ∣ D t

$D ::= [] \mid x \mid t \, D \mid D \, t$

\frac{}{(λ x . M) N \to_{n p} M {x \leftarrow N}} \frac{M \to_{n p} N}{D [M] \to_{n p} D [N]}

$\dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} \qquad \dfrac{M \to_{np} N}{D[M] \to_{np} D[N]}$

\frac{}{(λ x . M) N \to_{n p} M {x \leftarrow N}} (β) \frac{M \to_{n p} N}{M P \to_{n p} N P} (C_{@ <}) \frac{M \to_{n p} N}{P M \to_{n p} P N} (C_{@ >})

$\dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_{np} N}{M \, P \to_{np} N \, P} (C_{@\lt}) \qquad \dfrac{M \to_{np} N}{P \, M \to_{np} P \, N} (C_{@\gt})$

D

$D$ byłby nazywany kontekstem oceny, ponieważ służy do zdefiniowania pojęcia oceny. Kontekst oceny nie jest szczególnym rodzajem kontekstu; raczej, nazywając ją kontekst oceny jest to kwestia tego, co służy do kontekstu .

Podam jeszcze jeden przykład kontekstu. Zdefiniujmy wartości zgodnie z następującą składnią: Teraz zdefiniujmy inny rodzaj kontekstów: W porównaniu z powyżej, dziura może znajdować się po stronie funkcji aplikacji, jeśli argumentem aplikacji jest wartość. Zdefiniuj zatem następujące pojęcie redukcji: $V$

V ::= x V_{1} \dots V_{n} ∣ λ x . M

$V ::= x V_1 \ldots V_n \mid \lambda x. M$

E ::= [] ∣ M E ∣ E V

$E ::= [] \mid M \, E \mid E \, V$

D

$D$

\frac{}{(λ x . M) V \to_{c b v a} M {x \leftarrow V}} (β_{c b v a}) \frac{M \to_{β} N}{E [M] \to_{c b v a} E [N]} (γ_{c b v a})

$\dfrac{}{(\lambda x. M) \, V \to_{cbva} M \{x\leftarrow V\}} (\beta_{cbva}) \qquad \dfrac{M \to_\beta N}{E[M] \to_{cbva} E[N]} (\gamma_{cbva})$ Z zastrzeżeniem, że argument funkcji musi być wartością w pierwszej regule i że abstrakcje lambda nie są kontekstami, definiujemy strategię oceny call-by-value. Przy dalszym ograniczeniu, że argument jest oceniany przed funkcją, jest to wywołanie kolejności aplikacji według wartości.

— Gilles „SO- przestań być zły”
źródło

Twoja ostatnia definicja kontekstów oceny jest bliższa pierwotnemu pojęciu Felleisen i Hieb. Są to środki składniowe, które pomagają wyrazić kolejność oceny warunków rachunku różniczkowego. Kontekst ewaluacji jest szczególnym rodzajem kontekstu, ponieważ pozwala jednoznacznie rozdzielić pojęcie na kontekst i redeks (jeśli to możliwe), wskazując w ten sposób deterministycznie, gdzie powinien nastąpić następny krok redukcji.

— Dave Clarke

@DaveClarke Na marginesie możesz także użyć kontekstów oceny do zdefiniowania oceny dla niedeterministycznych pojęć obliczeń, w których nie masz unikalnego rozkładu na kontekst oceny i redeks.

— Martin Berger,

@MartinBerger: Indeedy.

— Dave Clarke

@DaveClarke Czy masz na myśli „ deterministyczny kontekst oceny jest szczególnym rodzajem kontekstu”? Potrafię wziąć dowolny zestaw kontekstów i na tej podstawie zdefiniować strategię oceny.

— Gilles „SO- przestań być zły”

@Gilles: Konteksty oceny mogą definiować deterministyczną strategię redukcji. Nie sądzę, że widziałem wyrażenie „deterministyczny kontekst oceny”. Są one oczywiście szczególnym rodzajem kontekstu. Zgadzam się z twoim komentarzem; chodzi o to, że twoja odpowiedź pomija historyczne znaczenie kontekstów oceny, które polegało na zdefiniowaniu deterministycznego pojęcia redukcji.

— Dave Clarke