Czy jest możliwe zaprezentowanie różnych strategii oceny poprzez modyfikację tego prostego reduktora?

Question

Jestem typem, który preferuje naukę, patrząc na kod, zamiast czytać długie wyjaśnienia. To może być jeden z powodów, dla których nie lubię długich prac naukowych. Kod jest jednoznaczny, zwarty, pozbawiony szumów, a jeśli czegoś nie dostajesz, możesz po prostu grać z nim - nie trzeba pytać autora.

Jest to pełna definicja rachunek lambda:

-- A Lambda Calculus term is a function, an application or a variable. 
data Term = Lam Term | App Term Term | Var Int deriving (Show,Eq,Ord) 

-- Reduces lambda term to its normal form. 
reduce :: Term -> Term 
reduce (Var index)  = Var index 
reduce (Lam body)  = Lam (reduce body) 
reduce (App left right) = case reduce left of 
    Lam body -> reduce (substitute (reduce right) body) 
    otherwise -> App (reduce left) (reduce right) 

-- Replaces bound variables of `target` by `term` and adjusts bruijn indices. 
-- Don't mind those variables, they just keep track of the bruijn indices. 
substitute :: Term -> Term -> Term 
substitute term target = go term True 0 (-1) target where 
    go t s d w (App a b)    = App (go t s d w a) (go t s d w b) 
    go t s d w (Lam a)    = Lam (go t s (d+1) w a) 
    go t s d w (Var a) | s && a == d = go (Var 0) False (-1) d t 
    go t s d w (Var a) | otherwise = Var (a + (if a > d then w else 0)) 

-- If the evaluator is correct, this test should print the church number #4. 
main = do 
    let two = (Lam (Lam (App (Var 1) (App (Var 1) (Var 0))))) 
    print $ reduce (App two two) 

Moim zdaniem funkcja „zmniejszyć” powyżej mówi znacznie więcej o rachunek lambda niż stron wyjaśnień i chciałabym po prostu patrzeć na kiedy zacząłem się uczyć. Możesz także zobaczyć, że wdraża bardzo rygorystyczną strategię oceny, która idzie nawet w obrębie abstrakcji. W tym duchu, jak zmodyfikować ten kod, aby zilustrować wiele różnych strategii ewaluacyjnych, które może mieć LC (wywołanie przez nazwę, leniwą ocenę, wywołanie po wartości, wywołanie przez dzielenie, częściową ocenę i wkrótce)?

Answer 1

połączeń według nazwy wymaga tylko kilku zmian:

1. nie dokonując oceny ciało abstrakcji lambda: reduce (Lam body) = (Lam body).

2. Brak oceny argumentu aplikacji. Zamiast tego, powinniśmy zastąpić go jak:

   reduce (App left right) = case reduce left of 
       Lam body -> reduce (substitute right body) 
   

Call-by-potrzeby (aka leniwy oceny) wydaje się trudniejsze (albo może być niemożliwe) do wdrożenia w pełni deklaratywny sposób, ponieważ musimy memoize wartości wyrażenia. Nie widzę sposobu, aby to osiągnąć z drobnymi zmianami.

Podział połączeń nie ma zastosowania do prostych obliczeń lambda, ponieważ nie mamy tu obiektów i przyporządkowań.

Możemy również użyć pełnej redukcji beta, ale musimy wybrać pewną deterministyczną kolejność oceny (nie możemy wybrać "arbitralnego" redeksu i zmniejszyć go za pomocą kodu, który mamy teraz). Ten wybór przyniesie pewną strategię oceny (możliwa jedna z opisanych powyżej).

Answer 2

Temat jest dość szeroki. Napiszę tylko o kilku pomysłach.

Proponowana reduce dokonuje równoległego przepisywania. Oznacza to, że mapuje ona App t1 t2 na App t1' t2' (pod warunkiem, że t1' nie jest abstrakcją). Niektóre strategie, takie jak CBV i CBN, są bardziej sekwencyjne, ponieważ mają tylko jeden redeks.

Aby je opisać, zmodyfikuję reduce, tak aby zwracała, czy faktycznie dokonano redukcji, czy też zamiast tego termin był normalną formą. Można to zrobić zwracając Maybe Term, gdzie Nothing oznacza normalną formę.

W ten sposób CBN byłoby

reduce :: Term -> Maybe Term 
reduce (Var index)   = Nothing -- Vars are NF 
reduce (Lam body)    = Nothing -- no reduction under Lam 
reduce (App (Lam body) right) = Just $ substitute right body 
reduce (App left right) = 
     (flip App right <$> reduce left) <|> -- try reducing left 
     (App left  <$> reduce right)  -- o.w., try reducing right 

podczas CBV byłoby

reduce :: Term -> Maybe Term 
reduce (Var index)   = Nothing 
reduce (Lam body)    = Nothing -- no reduction under Lam 
reduce (App (Lam body) right) 
    | reduce right == Nothing   -- right must be a NF 
    = Just $ substitute right body 
reduce (App left right) = 
     (flip App right <$> reduce left) <|> 
     (App left  <$> reduce right) 

Lazy oceny (z dzielenia) nie mogą być wyrażone za pomocą pojęć, jeśli dobrze pamiętam. Wymaga wykresów oznaczających, że subterm jest udostępniany.