Sto studiando Tipi e linguaggi di programmazione , e ho qualche problema a farmi un'idea dei concetti del 5 ° capitolo, The Untyped Lambda Calculus .
In particolare, redex , riduzione e le varie strategie di valutazione stanno facendo la mia testa. Quello che segue è ciò che ho capito nelle mie stesse parole, nel tentativo di spiegare cose a me stesso e ottenere più persone competenti per correggere i miei errori / imprecisioni. Sono sinceramente insicuro se questo è un formato accettabile per stackexchange e sono aperto a suggerimenti per renderlo più adatto.
Nota che altri hanno cercato di rispondere a una domanda molto simile, ma mi hanno comunque lasciato confuso:
- Chiama per valore nel calcolo lambda
- calcolo lambda non tipizzato: perché è call-by -valore rigoroso?
Redex
Se la mia comprensione è corretta, un redex è un'espressione riducibile, cioè l'applicazione di un termine lambda a un'astrazione lambda.
O, più concretamente, un redex ha sempre la forma (λx.s)t .
Riduzione Redex
La riduzione di (λx.s)t viene eseguita sostituendo tutte le occorrenze gratuite di x in s di t .
Ad esempio:
(λx.x + 2) 1
→ 1 + 2
→ 3
Il processo di riduzione di un'espressione lambda nella sua forma normale è guidato da una strategia di valutazione: un algoritmo per il prelievo che redex deve ridurre per primo. Per descriverli, tuttavia, abbiamo bisogno di un po 'più di vocabolario.
Qualifiche Redex
All'estrema sinistra e all'estrema destra
- il redex più a sinistra è quello la cui astrazione è testualmente a sinistra di tutti gli altri redex.
- il redex più a destra è quello la cui astrazione è testualmente a destra di tutti gli altri redex.
Quindi, ad esempio, in (λx.x + 2) (λy.y + 1) , abbiamo:
- leftex redex:
λx.x + 2 - rightex redex:
λy.y + 1
Ci può essere solo un redmost più a sinistra e uno a destra in una determinata espressione. Suppongo che in un'espressione composta da un singolo redex, quel redex sia il più a sinistra e più a destra.
Innermost e outbrost
- un redex più interno è uno che non contiene altri redex.
- un più esterno redex è contenuto in nessun altro redex.
Quindi, ad esempio, in (λx.(λy.y + 1) x) 2 , abbiamo:
- più interno:
λy.y + 1, poiché non contiene nessun altro redex. - più esterno:
λx.[...], poiché non è contenuto in nessun altro redex.
Suppongo che in un'espressione composta da un singolo redex, quel redex sia il più esterno e più interno.
Strategie di valutazione
Avendo definito questo, possiamo parlare delle due strategie di valutazione con cui sto combattendo: chiama per nome e chiama per valore .
Chiama per nome
In chiama per nome , il redex più esterno più a sinistra viene sempre selezionato per la riduzione. Inoltre, nessuna riduzione può verificarsi all'interno di un'astrazione lambda. L'esempio dato da Tipi e linguaggi di programmazione è:
id (id (λz. id z)) # the leftmost, outermost redex is the very first id
→ id (λz. id z) # the leftmost, outermost redex is still the first id
→ λz. id z # there is no outermost redex remaining, we're done.
Non capisco la necessità che la definizione della strategia includa nessuna riduzione può verificarsi all'interno di un'astrazione lambda : ciò non è implicito dal fatto che solo i redex più esterni possono beneficiare di una riduzione?
Chiama per valore
In chiama per valore l'estremo più a destra redex viene sempre selezionato per la riduzione. L'esempio dato da Tipi e linguaggi di programmazione è:
id (id (λz. id z)) # the rightmost, outermost redex is the second id
→ id (λz. id z) # the rightmost, outermost redex is the first id
# (it's textualy on the left, but there is no redex to its right)
→ λz. id z # the only remaining redex is not outermost (it's contained within
# an abstraction) and cannot be reduced.