LCME Понедельник, 29.05.2017, 16:10
Главная | Регистрация | Вход Приветствую Вас Гость | RSS
[ Новые сообщения · Участники · Правила форума · Поиск · RSS ]
Страница 1 из 11
Форум » Билеты к экзаменам » Программирование » 04 Продвинутая Лямбда
04 Продвинутая Лямбда
freidomДата: Воскресенье, 27.12.2009, 20:17 | Сообщение # 1
Главный тут
Группа: Администраторы
Сообщений: 273
Репутация: 20
Статус: Offline
Упорядоченная пара и алгебраический тип. Вычитание 1. Бета-эквивалентность (WTF?). Y-комбинатор. Реализация вычисления факториала через Y-комбинатор.

Упорядоченной парой термов A и B называется терм \s.s A B. Таким образом, нетрудно придумать функции для работы с подобными конструкциями:

Code
pair = \a.\b.\s.s a b
fst = \p.p True
snd = \p.p False

В дальнейшем для удобства упорядоченные пары будут обозначаться как <A, B>.

Рассмотрим представление следующего алгебраического типа в лямбда-исчислении:

Code
type ('a, 'b) x = L of 'a | R of 'b;;

Такой тип позволяет функции возвращать значения двух разных типов =)
Итак, представление в лямбде:
Code
inL = \a.<True, a>
inR = \b.<False, b>
case = \p.\fa.\fb.((fst p) fa fb) (snd p)

Сравните это со следующими записями:
Code
fun a -> L a
fun b -> L b
fun p la lb -> match p with (True, a) -> fa a | (False, b) -> fb b

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

Вычитание единицы - весьма нетривиальный трюк. Говорят, он пришёл в голову другу Чёрча, когда тот сидел в кабинете у стоматолога, поэтому называется он "трюком зуба мудрости".
Заметим, что вычитание единицы из n - это то же самое, что прибавление к 0 (n - 1) единицы. Попробуем реализовать программу, выполняющую подобную операцию, на OCaml.

Code
let dec n =
       let rec dec acc c =
        if c < n then if (fst acc) then dec (true, (snd acc) + 1) (c + 1) else dec (true, snd acc) (c + 1) else snd acc in
       dec (false, 0) 0;;

Что-то вроде этого...
Получилось неплохо за одним исключением: сравнение c и n - это нехорошо. К счастью, в лямбде можно избавиться не только от сравнения, но и от второго аргумента функции, так как там числа устроены по-другому:
Code
Dec = \n.\f.\x.snd (n (\p.(fst p)?<True, f (snd p)>:<True, x>) <False, x>)

Штукенберг также давал ещё одну реализацию того же; я в ней не разобрался, но выглядит она... минималистически?
Code
Dec = \n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)

UPD: разобрался smile
http://en.wikipedia.org/wiki/Lambda_calculus
Приблизительно посередине статьи, раздел "Arithmetic in lambda calculus", подпункт "Predecessor".
Quote
The predecessor function defined by PRED n = n - 1 for a positive integer n and PRED 0 = 0 is considerably more difficult. The formula
PRED := λnfx.n (λgh.h (g f)) (λu.x) (λu.u)
can be validated by showing inductively that if T denotes (λgh.h (g f)), then T^(n)(λu.x) = (λh.h(f^(n-1)(x))) for n > 0.

Quote
Функция вычитания единицы, определённая как PRED n = n - 1 для натурального n и PRED 0 = 0 является намного более сложной. Формула
PRED := λnfx.n (λgh.h (g f)) (λu.x) (λu.u)
может быть проверена индукцией, если показать, что если T = (λgh.h (g f)), тогда T^(n) (λu.x) = (λh.h (f^(n-1) (x))) при n > 0.

И ещё одна реализация декремента:
Code
Φ := λx.pair (snd x) (Inc (snd x))
PRED := λn.fst (n Φ (pair 0 0))

Бета-эквивалентностью называется транзитивное, рефлексивное и симметричное замыкание
бета-редукции, либо симметричное замыкание бета-редуцируемости.

Y-комбинатором называется следующий терм:

Code
Y = \f.(\x.f (x x)) (\x.f (x x))

У него есть замечательное свойство: (Y F) -b> F (Y F)...

Попробуем применить Y-комбинатор для реализации факториала. (На самом деле, конечно, это можно сделать гораздо проще без него.) Сначала заметим, что Y - это почти что цикл while. В самом деле, рассмотрим следующий пример:

Code
T = \f.\x.(IsZero x) 1 (Mul x (f (Dec x)))
fact = Y T -b> ?

Это очень напоминает программу на ML:
Code
let rec fact x =
   if x = 0 then 1 else x * (fact (n - 1));;

Как нетрудно заметить, всё довольно просто...
 
Jack_WarGunOffДата: Понедельник, 28.12.2009, 19:06 | Сообщение # 2
Сержант
Группа: Друзья
Сообщений: 34
Репутация: 6
Статус: Offline
Сори за правку, но трюк зуба мудрости пришел в голову не Черчу, а его другу. Черч декру очень обрадовался, сказал что теперь на лямбде все реализуемо. Еще я не уверен что трюк зуба мудрости - тот код, который ты привел выше

Aquila non captat muscas - Орлы не ловят мух

Сообщение отредактировал Jack_WarGunOff - Понедельник, 28.12.2009, 19:07
 
freidomДата: Понедельник, 28.12.2009, 19:35 | Сообщение # 3
Главный тут
Группа: Администраторы
Сообщений: 273
Репутация: 20
Статус: Offline
исправлено
 
Форум » Билеты к экзаменам » Программирование » 04 Продвинутая Лямбда
Страница 1 из 11
Поиск:

Copyright Freidom © 2017 Хостинг от uCoz