deniok

В блоге у Филип(п)а Вадлера вот какой сегодня пост появился.

Рассмотрим тотальные предикаты над потоками булевых значений:

-- в этом потоке на i-ом месте ложь
pos     :: Int -> [Bool] -> Bool
pos i xs = not (xs !! i)

-- свертка логическим И отрицания первых i элементов потока даст истину
run :: Int -> [Bool] -> Bool
run i xs = and (map not (take i xs))

-- первые i элементов потока являют собой циклическое повторение False,True
alt :: Int -> [Bool] -> Bool
alt i x = take i x == take i (cycle [False,True])

-- первые i элементов потока не совпадают с первыми i элементами этого потока
fal :: Int -> [Bool] -> Bool
fal i x = not (take i x == take i x)

После минимального размышления ясно, что для первых трех предикатов можно предъявить поток, для которого этот предикат выполняется. Для четвертого предиката такого потока, ясное дело, не существует. Ясно ли это компьютеру? Можно ли написать универсальную процедуру

exists :: ([Bool] -> Bool) -> Bool
exists p = ????????????

которая бы возвращала True для тотальных предикатов над потоками, для которых есть удовлетворяющий ему поток, и False в противном случае?

Да, можно! (если бы не тотальность, то было бы нельзя)

exists :: ([Bool] -> Bool) -> Bool
exists p = p (epsilon p)

-- если существует поток, для которого верен p, возвращает этот поток
-- если такого потока не существует, возвращает произвольный поток
epsilon :: ([Bool] -> Bool) -> [Bool]
epsilon p = prefix (p (prefix True p)) p

-- то же, что и epsilon, но ограничивается потоками, начинающимися с b
prefix :: Bool -> ([Bool] -> Bool) -> [Bool]
prefix b p = b : epsilon (\x -> p (b : x))

Проверяем в GHCi:

*Bizarre> let test f i = (exists $ f i, take (i+3) (epsilon $ f i)) 
*Bizarre> test pos 5
(True,[True,True,True,True,True,False,True,True])
*Bizarre> test run 5
(True,[False,False,False,False,False,True,True,True])
*Bizarre> test alt 5
(True,[False,True,False,True,False,True,True,True])
*Bizarre> test fal 5
(False,[False,False,False,False,False,False,False,False])

См. также пост Martin Escardo Seemingly impossible functional programs, где похожие соображения изложены подробнее.