Редактирование: Haskell, 02 лекция (от 05 октября)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 31: | Строка 31: | ||
2) TRUE 1 (λx.xx)(λx.xx) →β и тут мы зациклились. | 2) TRUE 1 (λx.xx)(λx.xx) →β и тут мы зациклились. | ||
- | Получается, что в зависимости от порядка раскрытия, мы можем найти | + | Получается, что в зависимости от порядка раскрытия, мы можем найти лии не найти норм. форму. |
Строка 46: | Строка 46: | ||
Если мы здесь используем определение формальной системы, где есть эта конверсия (η: λx.Mx ⇒ M), то все эти конверсии происх. после β-редукции, в конце. | Если мы здесь используем определение формальной системы, где есть эта конверсия (η: λx.Mx ⇒ M), то все эти конверсии происх. после β-редукции, в конце. | ||
- | Определение 2. Аппликативная редукционная стратегия - способ редукции λ-терма, где на каждом | + | Определение 2. Аппликативная редукционная стратегия - способ редукции λ-терма, где на каждом шагевыбирается β-редакс, не содержащий других β-редаксов. |
- | В первом примере в первом случае была нормальная | + | В первом примере в первом случае была нормальная редукц. стратегия, в втором - аппликативная. Они моделир. следу алгоритмы работы в ЯП: при вызове функции иы иожем как вычисл. арг до передачи функции, так и передать их внутрь. В случае С всегда исп. аппликативная тсратегия. При этом может быть такая ситуация: функция исп. второй арг. только если первый не равен нулю. При этом, если мы подадим такой вызов: f(0, 3/0), то оно рухнет, хотя второй арг. даже не задействован. В первом сл. таокго не происх., но оно работает медленно. Поэтому норм. стратегия работает медленно, но всегда приводит к результатаы. В совр. функц. языках исп. модиф. стр., наз. ленивой норм. стратегйией. Идея в том, что мы всё ещё не вычисл. знач. выр., но вместо него мы исп. дерево, и передаём не всё дерево, а ссылку на него. Это позв. как ускорить процесс, так и всегда находить рез-т. Но в языке C существует пример исп. норм. стратегии: это встроенный оператор if. Именно опотму, что он встроенный (вы не можете написать свой такой же), он может её использовать. Мы вычисл. каждую из ветвей только после вычисл. условия. |
В языке haskell if можно определить следующим образом: | В языке haskell if можно определить следующим образом: | ||
Строка 59: | Строка 59: | ||
Вернёмся к λ-исчислению. Теперь понятно, каким образом происх вычисления. | Вернёмся к λ-исчислению. Теперь понятно, каким образом происх вычисления. | ||
- | Арифметика. Здесь | + | Арифметика. Здесь исп. нумералы Чёрча. Нумералы Чёрча это функция. |
Определим 0 как FALSE для удобства. | Определим 0 как FALSE для удобства. | ||
Строка 79: | Строка 79: | ||
эквивалентны. | эквивалентны. | ||
- | Немного сложнее будет с вычитанием. Существует расширение, | + | Немного сложнее будет с вычитанием. Существует расширение, позв. добавлять отр. числа, но лектор не видит смысла его показывать, там всё ещё сложнее и запись ещё длиннее. Поэтому, функция, которая произв. вычитание, или хотя бы уменьш. на единицу... мы должны опр. pred как функцию, возвр. пред. число или если 0 то 0. Для этого мы должны уметь опр., явл. ли число нулём. Предикат для этого запис. след. образом: |
iszero=λn.n(λx.FALSE)TRUE | iszero=λn.n(λx.FALSE)TRUE | ||
Попробуем раскрыть его для нуля: | Попробуем раскрыть его для нуля: | ||
iszero 0 → 0(λx.FALSE)TRUE → (λfx.x)(λx.FALSE)TRUE → TRUE | iszero 0 → 0(λx.FALSE)TRUE → (λfx.x)(λx.FALSE)TRUE → TRUE | ||
- | Легко проверить, что если бы вместо x было бы хотя бы fx, то получилось бы FALSE. | + | Легко проверить, что если бы вместо x было бы хотя бы fx, то получилось бы FALSE. Обр. внимание, как произв. вычисления: вычилсения произв. через функцию, перед. в аргументе. |
В случае pred мы можем записать его как | В случае pred мы можем записать его как | ||
Строка 91: | Строка 91: | ||
Это определение наиболее очевидно. | Это определение наиболее очевидно. | ||
- | Таким | + | Таким обр., имея нумерала Чёрча, мы не тр. от языка налич. арифметики, тем не менее, обычно она есть, дабы вычисл. работали быстрее. |
- | Далее, списки. Мы говорили, что λ- | + | Далее, списки. Мы говорили, что λ-исчисл это также способ моделир. структур данных. Попробуем смоделировать пару чисел. |
Определим пару как: | Определим пару как: | ||
PAIR=λxyf.fxy | PAIR=λxyf.fxy | ||
- | Что даёт это определение: если мы определим пару из двух чисел, которую мы потом будем | + | Что даёт это определение: если мы определим пару из двух чисел, которую мы потом будем исп, то редуц. это след. образом: |
PAIR 4 2 →β λf.f 4 2 | PAIR 4 2 →β λf.f 4 2 | ||
- | Это функция, которая, в зависимости от того, какой | + | Это функция, которая, в зависимости от того, какой арг. вы подадите, выдаёт первый элемент или второй (в терминах лиспа - car/cdr) |
CAR=FIRST=λp.p TRUE | CAR=FIRST=λp.p TRUE | ||
CDR = SND = λp.p FALSE | CDR = SND = λp.p FALSE | ||
Строка 105: | Строка 105: | ||
SND(PAIR 4 2) → (λp.p FALSE)(PAIR 4 2) → (PAIR 4 2)FALSE → (λf.f 4 2) FALSE → FALSE 4 2 → 2 | SND(PAIR 4 2) → (λp.p FALSE)(PAIR 4 2) → (PAIR 4 2)FALSE → (λf.f 4 2) FALSE → FALSE 4 2 → 2 | ||
- | С | + | С исп. пары можем определить лисповский список. Что это такое? Это пара, где первый элемент это элемент, а второй — указатель на вторую пару такого же вида, где второй элемент тоже указатель на пару, где второй элемент — nil. |
- | В лиспе конструктор списка — cons, первый элемент списка — car, получение хвоста списка — cdr. Также существует функция isnull, которая | + | В лиспе конструктор списка — cons, первый элемент списка — car, получение хвоста списка — cdr. Также существует функция isnull, которая возвр. T, если список пуст. |
(3 4 5) | (3 4 5) | ||
Строка 119: | Строка 119: | ||
car = λx.FIRST(SND x) | car = λx.FIRST(SND x) | ||
cdr = &lamda;x.SND(SND x) | cdr = &lamda;x.SND(SND x) | ||
- | Это уже можно | + | Это уже можно исп. как список. |
- | Не хватает одного | + | Не хватает одного эл-та Тьюринг-полного языка — цикла. Наиболее рпостым методом, с т. з. лектора, явл. рекурсия. Как её организовать? Всё тот же Хаскел Карри решил исп. опр. неподвижной точки. Неподвижная точка — такая точка из обл. опр. функции, что значение функции в этой точке развно этой точке. |
x — НТ f(x): x ∈ D(f), f(x) = x | x — НТ f(x): x ∈ D(f), f(x) = x | ||
Строка 127: | Строка 127: | ||
λf(λx.f(xx))(λx.f(xx)) — Y-комбинатор | λf(λx.f(xx))(λx.f(xx)) — Y-комбинатор | ||
- | Вообще говоря, комбинаторов | + | Вообще говоря, комбинаторов неподв. точки чущ. очень много. Для примера лектор напишет только один, написанный Аланом Тьюрингом: |
(λx.λy.(y(xxy)))(λx.λy.(y(xxy))) | (λx.λy.(y(xxy)))(λx.λy.(y(xxy))) | ||
- | Общее | + | Общее св-во этих комбинаторов одно: у них есть некоторая часть, которая повт. Св-во на саомм деле, если мы попр. раск. комб. и подст. функцию, то его можно записать след. обазом: |
Для некоторого ∀a∈Λ Ya=a(Ya) | Для некоторого ∀a∈Λ Ya=a(Ya) | ||
- | Как это | + | Как это исп. для рекурсии? Попр. записать опр. факториала: |
n! = 1, если n=0; n(n-1)! | n! = 1, если n=0; n(n-1)! | ||
- | Для | + | Для опр. факт. требуется цикл. Опр. функцию итерация факториала: |
IFACT=λf.λn.if(iszero n) 1 (mult n (f (pred n))) | IFACT=λf.λn.if(iszero n) 1 (mult n (f (pred n))) | ||
после чего вычислим | после чего вычислим | ||
(Y IFACT)5 = IFACT (Y IFACT) 5 | (Y IFACT)5 = IFACT (Y IFACT) 5 | ||
- | Таким | + | Таким обр. мы можем видеть что аппара λ-исчисл. явл. Тьюринг-полным, несмотря на то, что мы не имеем переменных, не имеем ..., орг. всё мы можем. |
- | Так как | + | Так как ф. языки осн. на λ-исчисл, а в λ-исчисл. аппаратом для орг. итеративных выч. исп. рекурсия, то она же исп. и для ФЯП. |
{{Haskell}} | {{Haskell}} | ||
{{Lection-stub}} | {{Lection-stub}} |