John Harrison - Введение в функциональное программирование (1108517), страница 20
Текст из файла (страница 20)
В качестве примера представимтерм λx y. y (x x y) с помощью:Abs("x",Abs("y",Comb(Var "y",Comb(Comb(Var "x",Var "x"),Var "y"))))Вот определение рекурсивной функции free_in, определяющей является липеременная в терме свободной:#let rec free_in x =fun (Var v) -> x = v| (Const c) -> false| (Comb(s,t)) -> free_in x s or free_in x t| (Abs(v,t)) -> not x = v & free_in x t;;free_in : string -> term -> bool = <fun>#free_in "x" (Comb(Var "f",Var "x"));;- : bool = true#free_in "x" (Abs("x",Comb(Var "x",Var "y")));;- : bool = falseТочно так мы можем по рекурсии определить подстановку.
Сначала, во избежаниеконфликта имён, нам потребуется функция для переименования переменных. Мыхотим преобразовывать существующие имена переменных в новые, связанные взаданном выражении. Переименование производится путём добавления символа.#let rec variant x t =if free_in x t then variant (x^"’") telse x;;variant : string -> term -> string = <fun>#variant "x" (Comb(Var "f",Var "x"));;- : string = "x’"#variant "x" (Abs("x",Comb(Var "x",Var "y")));;- : string = "x"#variant "x" (Comb(Var "f",Comb(Var "x",Var "x’")));;- : string = "x’’"Теперь мы можем определить подстановку так, как мы это сделали для абстрактныхтермов:76Глава 6. Более подробно о ML6.3.
Определения типов#let rec subst u (t,x) =match u withVar y -> if x = y then t else Var y| Const c -> Const c| Comb(s1,s2) -> Comb(subst s1 (t,x),subst s2 (t,x))| Abs(y,s) -> if x = y then Abs(y,s)else if free_in x s & free_in y t thenlet z = variant y (Comb(s,t)) inAbs(z,subst (subst s (Var y,z)) (t,x))else Abs(y,subst s (t,x));;subst : term -> term * string -> term = <fun>Обратите внимание на очень близкие параллели между стандартнымматематическим представлением лямбда - исчисления, что обсуждалось ранее,и ML версией.
Всё что нам действительно надо для завершения аналогии, этовместо явного вызова конструкторов читать и записывать термы в более удобнойформе. Мы вернёмся к этой проблеме позже и обсудим как можно добавить такиевозможности.6.3.4Тонкости рекурсивных типовРекурсивный тип может содержать вложенные конструкторы других типов,включая конструктор типа функций. Например, рассмотрим следующий код:#type (’a)embedding = K of (’a)embedding->’a;;Type embedding defined.Если мы задумаемся о нижележащей семантике, то увидим, ситуацияпредставляется серьёзной. Рассмотрим, к примеру, специальный случай,когда ’a является bool.
У нас также есть инъективная функцияK:((bool)embedding->bool)->(bool)embedding. А это прямо противоречиттеореме Кантора о том, что множество всех подмножеств множества X неможет быть инъективно ему.4 Следовательно, рассуждая о типах, нам следуетбыть более осторожными. В действительности, α → β не может рассматриватьсякак полное функциональное пространство. Иначе конструкции рекурсивных типовбудут противоречивы. Поскольку все функции, которые мы можем задать, вдействительности являются вычислимыми, есть смысл ограничиться только ими. Стаким ограничением семантика будет непротиворечива, хотя детали усложнятся.Рассмотренное определение также имеет интересные последствия для системытипов. Например, мы можем теперь определить Y комбинатор, используя Kдля приведения типа. Заметьте, если K удалёны, мы имеем, в сущности,обычное определение Y комбинатора в нетипизированном лямбда - исчислении.Конструкция let используется всего лишь для эффективности, но мы нуждаемсяв η-редексе включающем z для предупреждения зацикливания в стратегиивычисления принятой в ML.4Доказательство: рассмотрим C = {i(s) | s ∈ ℘(X) и i(s) 6∈ s}.
Если i : ℘(X) → X инъективно,выполняется i(C) ∈ C ⇔ i(C) 6∈ C, получили противоречие. Эта конструкция напоминает парадоксРассела, и, возможно, в действительности вдохновлена им. Аналогия будет ещё более близкой, еслимы рассмотрим равнозначное утверждение о несюръективности j : X → ℘(X), и докажем это,рассматривая {s | s 6∈ j(s)}.776.3. Определения типовГлава 6. Более подробно о ML#let Y h =let g (K x) z = h (x (K x)) z ing (K g);;Y : ((’a -> ’b) -> ’a -> ’b) -> ’a -> ’b = <fun>#let fact = Y (fun f n -> if n = 0 then 1 else n * f(n - 1));;fact : int -> int = <fun>#fact 6;;- : int = 720Итак, рекурсивные типы представляют собой значительный вклад в язык ипозволяют нам обойтись без задания оператора рекурсии примитивой языка.Упражнения1. Что будет неверно в нашем определении subst, если мы заменимVar y -> if x = y then t else Var yследующим фрагментом? Var x -> t | Var y -> Var y2.
Можно было бы, определить (хотя это неэффективно) натуральные числапосредством следующего рекурсивного типа:#type num = Zero | Suc of num;;Напишите функции, выполняющие арифметические действия над числами вэтой форме.3. Используйте определение типа для синтаксиса лямбда - термов, что мы даливыше. Напишите функцию, конвертирующую произвольный лямбда - термв эквивалент, записанный с помощью S, K и I комбинаторов.
Представьтекомбинаторы с помощью Const "S", используйте технику, рассмотренную намиранее.4. Расширьте синтаксис лямбда - термов, включив типизацию в стиле Чёрча. Writefunctions that check the typing conditions before allowing terms to be formed, butotherwise map down to the primitive constructors.5. Рассмотрим тип бинарных деревьев со строками в узлах:#type stree = Leaf | Branch of stree * string * stree;;Напишите функцию strings, возвращающую список строк, полученный приобходе дерева в порядке слева на право. Напишите функцию, котораяпринимает строку и дерево, для которого соответствующий список сортированв алфавитном порядке, а возвращает дерево, со строкой, вставленнной ссохранением упорядоченности.78Глава 6.
Более подробно о ML6.3. Определения типов6. (*) Улучшите эти функции так, чтобы на каждом шагу дерево оставалосьпочти балансированным, т.е. для каждого узла максимальная глубина левогои правого поддерева отличалась не более чем на единицу.57. (*) Можете ли вы описать типы выражений, которые могут быть записаныв типизированном лямбда - исчислении, без оператора рекурсии?6 Каков типследующей рекурсивной функции?l e t rec f i = ( i o f ) ( i o i ) ; ;Покажите как это может использоваться для записи ML выражений сполностью полиморфным типом α.
Можете ли вы написать завершённоевыражение с таким свойством? Как насчёт произвольной функции типа α → β?5За подробностями об этих «АВЛ деревьях» и похожих методах для балансированных деревьевобращайтесь к Adel’son-Vel’skii and Landis (1962) и различным книгам по алгоритмам.6Ответ лежит в «гомоморфизме Карри-Говарда» – для подробностей см. Girard, Lafont, andTaylor (1989).796.3. Определения типовГлава 6. Более подробно о ML80Глава 7Доказательство корректностипрограммПрограммисты не раз убеждались на своём горьком опыте как бываетсложно написать корректную программу, то есть такую, которая делает вточности то, что требуется.
В большинстве объёмных программ есть ошибки,последствия которых могут быть самыми различными. Некоторые ошибкибезобидны, другие — раздражают, а некоторые — смертельно опасны. Кпримеру, программное обеспечение электрокардиостимуляторов, автопилотов,систем управления двигателями, антиблокировочных тормозных систем, прибороврадиационной терапии, систем управления ядерных реакторов критично к наличиюошибок.
Ошибки, допущенные при разработке таких программ, могут повлечь засобой массовые человеческие жертвы. Чем глубже проникновение компьютеров вовсе сферы жизни человечества, тем серьёзнее возможная угроза жизни людей,порождаемая ошибками в программах. 1Каким образом мы можем убедиться в корректной работе программы? Одним изполезных методов будет тестирование программы на обширном наборе планируемыхсценариев её использования. При этом входные данные для тестов подбираютсятак, чтобы проверить различные составляющие программы в поисках возможныхошибок. В реальности оказывается, что потенциальных вариантов использованияслишком много, чтобы полностью проверить все из них, так что некоторые ошибкимогут быть пропущены в ходе тестирования.
Как неоднократно подчёркивают многиеавторы, в частности, Дейкстра, тестирование программ может быть полезным длядемонстрации наличия ошибок, но показать их отсутствие оно в состоянии лишь вотдельных редких случаях.Альтернативой тестированию программ служит возможность их математическойверификации.
Программа, реализованная на достаточно точно определённом языкепрограммирования, имеет однозначное математическое толкование. Аналогично,требования к программе могут быть выражены на языке математики и логикикак точная спецификация. Такая формализация открывает возможность строгогодоказательства соответствия программы и спецификации.Чтобы лучше ощутить разницу между тестированием и верификацией,1Аппаратное обеспечение подвержено схожим проблемам, но мы будем рассматриватьисключительно программы.81Глава 7. Доказательство корректности программрассмотрим следующее простое отношение:ΣNn=0 n =N (N + 1)2Утверждается, что оно справедливо для произвольных значений N .
Мы, очевидно,в состоянии проверить его для любого количества избранных N . Такая проверкаможет привести нас к интуитивной уверенности в корректности формулы, посколькувыглядит маловероятным, что она когда-либо окажется ложной. Однако, в общемслучае попытки сделать выводы по свойствам эмпирических данных могут ввестив заблуждение. В теории чисел известно немало примеров утверждений, которыев итоге опровергались, несмотря на множество положительных частных случаев.2Более надёжный подход — математическое доказательство справедливостиприведённого утверждения, что легко достигается путём индукции по переменной N .Аналогично, мы можем надеяться заменить тестирование программы на некоторомконечном множестве входных данных формальным доказательством корректностиеё функционирования в общем случае.
В то же время, следует признать, чтоверификация имеет свои границы применимости.• Требуется гарантировать, что процесс выполнения программы компьютеромв точности соответствует абстрактной математической модели. Возможнойпричиной расхождений могут стать ошибки в компиляторах или операционныхсистемах, а также физические дефекты аппаратуры. Такие проблемы,безусловно, присущи любым попыткам применения математики в естественныхнауках. К примеру, предположение точного соответствия между машиннойреализацией арифметических операций и их математическими прообразамиявляется естественным упрощением моделей, подобно тому, как при анализепростых динамических систем пренебрегают сопротивлением воздуха.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
