2013-03-27

deniok: (Default)
2013-03-27 11:55 am

Трудности с простыми лямбда-калькуляторами

А вот, кстати, при проверке лямбда-калькуляторов, написанных студентами, возникла такая задачка.

Пускай мы реализовали на Хаскелле лямбда-термы
data Term = 
    Var String
  | App Term Term
  | Lam String Term        
проверку их альфа-эквивалентности (можно и точное совпадение, для наших целей не важно):
alphaEq :: Term -> Term -> Bool
и одношаговую бета-редукцию (нормальную, для определенности, хотя это тоже не важно):
reduce :: Term -> Term
В последнем случае при отсутствии редексов просто возвращается исходный терм.

Если мы теперь хотим реализовать многошаговую бета-редукцию до нормальной формы, мы можем итерировать, делая шаг редукции до тех пор, пока терм не перестанет меняться. Ну, например, так
reduceToNF :: Term -> [Term]
reduceToNF = unfoldr step where 
  step t = 
      let next = reduсe t in 
    if t `alphaEq` next 
    then Nothing 
    else Just (t, next)


Не видите ли вы червоточины в этой схеме?