Экзамен Хохряков. Равенство лямбдатермов. Именованные выражения в лямбдатермах
 Скачать 214.61 Kb.
|
|
Хохряков Д., 220681 Вариант №15 Равенство лямбда-термов. Именованные выражения в лямбда-термах. Let конструкция в Haskell. Преобразование целых чисел в действительные в Haskell.. Обобщенное правило резолюции. Кортежи в F#. Вычислить значение лямбда выражения  Построить комбинатор, который определяет по натуральному числу следующую функцию (n,m) → n –4*m Написать функцию на языке Haskell для нахождения максимального элемента списка. Приложить ссылку на видео работы программы. Написать предикат в Prolog для нахождения количества положительных элементов в списке. Приложить ссылку на видео работы программы. Ответы Два терма равны, если от одного из них можно перейти к другому с помощью конечной последовательности конверсий. Определим понятие равенства следующими выражениями, в которых горизонтальные линии следует понимать как: «если утверждение над чертой выполняется, то выполняется и утверждение под ней».  Следует отличать понятие равенства, определяемое этими формулами, от понятия синтаксической эквивалентности, которую будем обозначать специальным символом ≡. Например, λх.х ≠ λу.у, но λх.х = λу.у. Можно рассматривать синтаксическую эквивалентность термов с точностью до α-конверсий. Такую эквивалентность обозначают символом  . Это отношение определяется так же, как равенство лямбда-термов, за тем исключением, что из всех конверсий допустимы только α -конверсии. Таким образом,  .Рекурсивные функции можно определить, не вводя каких-либо имен. Тем не менее возможность давать имена выражениям часто бывает полезна, поскольку позволяет избежать долгих и утомительных повторений. Простая форма именования может быть введена как форма «синтаксического сахара» над чистым лямбда-исчислением:  Например:  В композиционном стиле функция вычисления площади треугольника будет выглядеть так: square a b c = let p = (a + b + c) / 2 in sqrt (p * (p - a) * (p - b) * (p - c)) Слова let и in – ключевые. Выгодным отличием let-выражений является то, что они являются обычными выражениями и не привязаны к определённому месту как where-выражения. Они могут участвовать в любой части обычного выражения: square a b c = let p = (a + b + c) / 2 in sqrt ((let pa = p - a in p * pa) * (let pb = p - b pc = p - c in pb * pc)) В этом проявляется их принадлежность композиционному стилю. let-выражения могут участвовать в любом подвыражении, они также группируются скобками. А where-выражения привязаны к уравнениям в определении функции. Также как и в where-выражениях, в let-выражениях слева от знака равно можно проводить декомпозицию значений. pred :: Nat -> Nat pred x = let (Succ y) = x in y Для преобразования целых чисел в действительные используется функция fromIntegral. Из истинности двух дизъюнкций, одна из которых содержит дизъюнкт, а другая – его отрицание, следует (выводима) формула, являющаяся дизъюнкцией исходных формул без упомянутого дизъюнкта и его отрицания. Две фразы могут быть резольвированы друг с другом, если одна из них содержит позитивный литерал, а другая – соответствующий негативный литерал с одним и тем же обозначением предиката и одинаковым количеством аргументов, причем аргументы обоих литералов могут быть унифицированы (то есть согласованы) друг с другом. Резольвента – истинная формула, получающаяся в результате подстановки в дизъюнкцию исходных формул после удаления в них соответствующих литералов. Обобщенное правило резолюции    Подстановка   Кортеж — это группирование неименованных, но упорядоченных значений, возможно, для разных типов. Кортежи могут быть либо ссылочными типами, либо структурами. Их можно рассматривать как сами значения или как значения, агрегированные из других значений. Они имеют множество применений, например, удобный возврат нескольких значений из функции или группирование значений для некоторого нерегламентированного удобства. module Tuples = /// A simple tuple of integers. let tuple1 = (1, 2, 3) /// A function that swaps the order of two values in a tuple. /// /// F# Type Inference will automatically generalize the function to have a generic type, /// meaning that it will work with any type. let swapElems (a, b) = (b, a) printfn $"The result of swapping (1, 2) is {(swapElems (1,2))}" /// A tuple consisting of an integer, a string, /// and a double-precision floating point number. let tuple2 = (1, "fred", 3.1415) printfn $"tuple1: {tuple1}\ttuple2: {tuple2}"  Построить комбинатор, который определяет по натуральному числу следующую функцию (n,m) → n –4*m Написать функцию на языке Haskell для нахождения максимального элемента списка. Приложить ссылку на видео работы программы. https://yadi.sk/i/zaga2LiUCE0Xag  import Data.List (foldl1') import System.IO maximum' :: Ord a => [a] -> a maximum' = foldl1' max getInput :: IO [Int] getInput = readLn main :: IO () main = do putStrLn "Input integers:" xs <- getLine print . maximum . map (read :: String -> Int) . words $ xs Написать предикат в Prolog для нахождения количества положительных элементов в списке. Приложить ссылку на видео работы программы. https://yadi.sk/i/kPGH11q4dwWdzw  implement main open core, console class predicates countPositive : (integer*, integer [out]). clauses countPositive([], 0). countPositive([H | T], N) :- countPositive(T, N1), if H > 0 then N = N1 + 1 else N = N1 end if. run() :- init(), List = [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5], countPositive(List, N), writef("Количество положительных чисел: %", N), nl, write("Для продолжения нажмите любую клавишу . . ."), _ = readLine(). end implement main goal console::runUtf8(main::run). |