Диссертация (1150902), страница 19

Файл №1150902 Диссертация (Трассирующая нормализация) 19 страницаДиссертация (1150902) страница 192019-06-292019-06-29СтудИзба

Трассирующая нормализация

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Регистрация/авторизация

Текст из файла (страница 19)

129–145.90. Launchbury, J. A Natural Semantics for Lazy Evaluation / J. Launchbury // Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, Charleston, South Carolina, USA, January 1993. — 1993. — P. 144–154.91. Abramsky, S. Full Abstraction in the Lazy Lambda Calculus / S. Abramsky, C.H. L. Ong // Inf.

Comput. — 1993. — Vol. 105, no. 2. — P. 159–267.92. Blum, W. Imaginary Traversals for the Untyped Lambda Calculus (ongoingwork) / W. Blum. — 2017.93. Jones, N. D. Transformation by interpreter specialisation / N. D. Jones // Sci. Comput. Program. — 2004. — Vol. 52. — P. 307–339.94. Березун, Д. А. Трассирующая нормализация нетипизированного лямбдаисчисления / Д. А. Березун // Известия вузов. Северо Кавказский регион.Технические науки. — 2017.

— № 4. — С. 5–12.10895. Березун, Д. А. Полная головная линейная редукция / Д. А. Березун // Научнотехнические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление. — 2017. — Т. 10, № 3. — С. 59–82.96. Launchbury, J. A Strongly-Typed Self-Applicable Partial Evaluator / J.

Launchbury // Lecture Notes in Computer Science, Functional Programming Languagesand Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings / Ed. by J. Hughes. — Vol. 523. — Springer,1991. — P. 145–164.97. Glück, R. Is there a fourth Futamura projection? / R.

Glück // Proceedings of the2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-basedProgram Manipulation, PEPM 2009, Savannah, GA, USA, January 19-20, 2009 /Ed. by G. Puebla, G. Vidal. — ACM, 2009. — P. 51–60.98. Gomard, C. K. Partial Type Inference for Untyped Functional Programs /C. K. Gomard // LISP and Functional Programming. — 1990. — P. 282–287.99. Bondorf, A.

Improving Binding Times Without Explicit CPS-Conversion /A. Bondorf // LISP and Functional Programming. — 1992. — P. 1–10.100. Birkedal, L. Hand-Writing Program Generator Generators / L. Birkedal, M. Welinder // Lecture Notes in Computer Science, Programming Language Implementation and Logic Programming, 6th International Symposium, PLILP’94, Madrid,Spain, September 14-16, 1994, Proceedings / Ed. by M. V.

Hermenegildo, J. Penjam. — Vol. 844. — Springer, 1994. — P. 198–214.101. Statman, R. The Typed lambda-Calculus Is not Elementary Recursive / R. Statman // 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977. — IEEE ComputerSociety, 1977. — P. 90–94.102. Jones, N. D. Call-by-Value Termination in the Untyped lambda-Calculus /N. D.

Jones, N. Bohr // Logical Methods in Computer Science. — 2008. — Vol. 4,no. 1.109103. Kahn, G. Natural Semantics / G. Kahn // Lecture Notes in Computer Science,STACS 87, 4th Annual Symposium on Theoretical Aspects of Computer Science,Passau, Germany, February 19-21, 1987, Proceedings / Ed. by F.-J. Brandenburg,G. Vidal-Naquet, M. Wirsing. — Vol. 247. — Springer, 1987. — P. 22–39.104. Plotkin, G. D. A structural approach to operational semantics / G. D. Plotkin // J.Log.

Algebr. Program. — 2004. — Vol. 60-61. — P. 17–139.105. Hennessy, M. Semantics of programming languages - an elementary introductionusing structural operational semantics / M. Hennessy. — Wiley, 1990.106. Grégoire, B. A compiled implementation of strong reduction / B. Grégoire,X. Leroy // Proceedings of the Seventh ACM SIGPLAN International Conferenceon Functional Programming (ICFP ’02), Pittsburgh, Pennsylvania, USA, October4-6, 2002. / Ed. by M. Wand, S. L.

P. Jones. — ACM, 2002. — P. 235–246.107. Экспериментальнаямализацииресурс].реализациянетипизированного—URL:алгоритматрассирующейлямбда-исчислениянор-[Электронныйhttps://github.com/danyaberezun/traversal-Based-Normalization (дата обращения: 10.12.2017).110Список рисунков1Именованное представление чистого лямбда-исчисления . . . . . .

162Неименованное представление чистого лямбда-исчисления . . . . . 173η-конверсия . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174Простое типизированное лямбда-исчисление в стиле Карри . . . . . 185Простое типизированное лямбда-исчисление в стиле Чёрча . . . . . 1967Пример: деревья Бёма для термов, не имеющих нормальной формы 24Терм mul ⃗2 ⃗2, его η-длинная форма и её АСД . . .

. . . . . . . . . . 268Определение списков головных абстракций и простых редексов . . 279Система переходов для головной линейной редукции . . . . . . . . 3510Поведение системы переходов для головной линейной редукциина примере терма (λ x . x) @ (λ y . y) . . . . . . . . . . . . . . .

. . 3611Иллюстрация к теореме 2 . . . . . . . . . . . . . . . . . . . . . . . 3912Терм M [λy] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4213Система переходов для полной головной линейной редукции . . . . 4414Слабая редукция . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . 4715Строгая редукция . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4716Строгая редукция, основанная на окружении . . . . . . . . . . . . . 4817Строгая хвосто-рекурсивная редукция . . . . . . . . . . . . . . . . . 4918Семантика, основанная на истории и окружении . . . . . . . . . . .

5119Алгоритм трассирующей нормализации для нетипизированного2021лямбда-исчисления . . . . . . . . . . . . . . . . . . . . . . . . . . . 53АСД терма mul ⃗2 ⃗2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54Результат работы UNP на терме mul ⃗2 ⃗2 . . . . . . . . . . . . . . . . 5622Система переходов для BUNP . . . .

. . . . . . . . . . . . . . . . . 5823Иллюстрация к Теореме 4 . . . . . . . . . . . . . . . . . . . . . . . . 6211124Правила переходов для UNP . . . . . . . . . . . . . . . . . . . . . . 6625Иллюстрация к Теореме 5 . . . . . . . . . . . . . . . . . . . . . . .

. 6927Результат применения “The Trick” к функции evaloperand и статическому аргументу e . . . . . . . . . . . . . . . . . . . . . . . . . . . 8026Аннотированная версия алгоритма трассирующей нормализациидля нетипизированного лямбда-исчисления . . . . . . . . . . .

. . . 8128Аннотированная версия функции evaloperand . . . . . . . . . . . . 8229Результат компиляции программы . . . . . . . . . . . . . . . . . . . 8330Правила переходов для случаев применения, абстракции и связанной переменной . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8731Правила переходов для случая свободной переменной . . . . . . . .

8832Естественная семантика нетипизированного лямбда-исчисления,основанная на окружении и соответствующая аппликативному порядку редукции . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9233Обход терма sum 1 . . . . . . . . . . . . . .

. . . . . . . . . . . . . . 9434Трассирующая семантика новых языковых конструкций . . . . . . 95112Список таблиц1Нормальные формы . . . . . . . . . . . . . . . . . . . . . . . . . . . 20113Приложение A. Примерисполнения программ на LLLВ приложении представлено исполнение программы mul ⃗2 ⃗2 на языке LLL.Исполнение состоит из вызовов функций (например, lz1 = bind @4), между которыми приведены текущие значения динамических стеков, представляющих соответствующие указатели алгоритма трассирующей нормализации.[][]@01 = apply @02 data2[(data2,[])][]@02 = apply mul data1[(data2,[]), (data1,[])][]lm = bind ln[(data2,[])][(data1,[])]ln = bind lS[][(data2,[]), (data1,[])]lS = bind lZ[][bot, (data2,[]), (data1,[])]lZ = bind @1[]114[bot, bot, (data2,[]), (data1,[])]@1 = apply @2 Z[(Z,[bot, bot, (data2,[]), (data1,[])])][bot, bot, (data2,[]), (data1,[])]@2 = apply m @3[(@3,[bot, bot, (data2,[]), (data1,[])]), (Z,[bot,,→ bot, (data2,[]), (data1,[])])][bot, bot, (data2,[]), (data1,[])]m = getV 3[(@3,[bot, bot, (data2,[]), (data1,[])]), (Z,[bot,,→ bot, (data2,[]), (data1,[])])][]data1 = ls1 = bind lz1[(Z,[bot, bot, (data2,[]), (data1,[])])][(@3,[bot, bot, (data2,[]), (data1,[])])]lz1 = bind @4[][(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,[bot,,→ bot, (data2,[]), (data1,[])])]@4 = apply s1 @5[(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])])][(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,[bot,,→ bot, (data2,[]), (data1,[])])]s1 = getV 1[(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])])][bot, bot, (data2,[]), (data1,[])]@3 = apply n S[(S,[bot, bot, (data2,[]), (data1,[])]),(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])])][bot, bot, (data2,[]), (data1,[])]115n = getV 2[(S,[bot, bot, (data2,[]), (data1,[])]),(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])])][]data2 = ls2 = bind lz2[(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])])][(S,[bot, bot, (data2,[]), (data1,[])])]lz2 = bind @6[][(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])]),(S,[bot, bot, (data2,[]), (data1,[])])]@6 = apply s2 @7[(@7, [(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]),→ , (@3,[bot, bot, (data2,[]), (data1,[])])]),(S,[bot, bot, (data2,[]), (data1,[])])])][(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])]),(S,[bot, bot, (data2,[]), (data1,[])])]s2 = getV 1[(@7, [(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]),→ , (@3,[bot, bot, (data2,[]), (data1,[])])]),(S,[bot, bot, (data2,[]), (data1,[])])])][bot, bot, (data2,[]), (data1,[])]S = getV 1[(@7, [(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]),→ , (@3,[bot, bot, (data2,[]), (data1,[])])]),(S,[bot, bot, (data2,[]), (data1,[])])])][]bot = continue[]116[(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])]),(S,[bot, bot, (data2,[]), (data1,[])])]@7 = apply s2 z2[(z2,[(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]),,→(@3,[bot, bot, (data2,[]), (data1,[])])]),(S,[bot, bot, (data2,[]), (data1,[])])])][(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])]),(S,[bot, bot, (data2,[]), (data1,[])])]s2 = getV 1[(z2,[(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]),,→(@3,[bot, bot, (data2,[]), (data1,[])])]),(S,[bot, bot, (data2,[]), (data1,[])])])][bot, bot, (data2,[]), (data1,[])]S = getV 1[(z2,[(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]),,→(@3,[bot, bot, (data2,[]), (data1,[])])]),(S,[bot, bot, (data2,[]), (data1,[])])])][]bot = continue[][(@5, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])]),(S,[bot, bot, (data2,[]), (data1,[])])]z2 = getV 0[][(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,[bot,,→ bot, (data2,[]), (data1,[])])]@5 = apply s1 z1[(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])])]117[(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,[bot,,→ bot, (data2,[]), (data1,[])])]s1 = getV 1[(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])])][bot, bot, (data2,[]), (data1,[])]@3 = apply n S[(S, [bot, bot, (data2,[]), (data1,[])]),(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])])][bot, bot, (data2,[]), (data1,[])]n = getV 2[(S, [bot, bot, (data2,[]), (data1,[])]),(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])])][]data2 = ls1 = bind lz1[(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])])][(S, [bot, bot, (data2,[]), (data1,[])])]lz1 = bind @4[][(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])]),(S, [bot, bot, (data2,[]), (data1,[])])]@4 = apply s1 @5[(@5, [(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]),→ , (@3,[bot, bot, (data2,[]), (data1,[])])]),(S, [bot, bot, (data2,[]), (data1,[])])])][(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])]),(S, [bot, bot, (data2,[]), (data1,[])])]s1 = getV 1118[(@5, [(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]),→ , (@3,[bot, bot, (data2,[]), (data1,[])])]),(S, [bot, bot, (data2,[]), (data1,[])])])][bot, bot, (data2,[]), (data1,[])]S = getV 1[(@5, [(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]),→ , (@3,[bot, bot, (data2,[]), (data1,[])])]),(S, [bot, bot, (data2,[]), (data1,[])])])][]bot = continue[][(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])]),(S, [bot, bot, (data2,[]), (data1,[])])]@5 = apply s1 z1[(z1, [(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]),→ , (@3,[bot, bot, (data2,[]), (data1,[])])]),(S, [bot, bot, (data2,[]), (data1,[])])])][(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])]),(S, [bot, bot, (data2,[]), (data1,[])])]s1 = getV 1[(z1, [(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]),→ , (@3,[bot, bot, (data2,[]), (data1,[])])]),(S, [bot, bot, (data2,[]), (data1,[])])])][bot, bot, (data2,[]), (data1,[])]S = getV 1[(z1, [(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]),→ , (@3,[bot, bot, (data2,[]), (data1,[])])]),(S, [bot, bot, (data2,[]), (data1,[])])])][]bot = continue[]119[(z1, [(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,→ ,[bot, bot, (data2,[]), (data1,[])])]),(S, [bot, bot, (data2,[]), (data1,[])])]z1 = getV 0[][(Z,[bot, bot, (data2,[]), (data1,[])]), (@3,[bot,,→ bot, (data2,[]), (data1,[])])]Z = getV 0[][bot, bot, (data2,[]), (data1,[])]bot = THE END120Приложение Б.Пример работы системы переходов для алгоритматрассирующей нормализации, соответствующегоаппликативному порядку редукцииВ приложении приведен пример работы системы переходов для алгоритматрассирующей нормализации для нетепизированного лямбда-исчисления, соответствующего аппликативному порядку редукции, представленный в разделе 6.1,на примере терма mul ⃗2 ⃗2, АСД которого приведено на рис.

Характеристики

Тип файла

PDF-файл

Размер

1,34 Mb

Материал

Трассирующая нормализация

Тип материала

Кандидатская диссертация

Предмет

Физико-математические науки

Высшее учебное заведение

СПбГУ

Список файлов диссертации

trassirujuschaja-normalizacija.rar

Трассирующая нормализация

Автореферат.pdf

Выписка из протокола заседания диссертационного совета.pdf

Диссертация.pdf

Информация об официальном оппоненте 2.pdf

Информация об официальном оппоненте.pdf

Отзыв ведущей организации.pdf

Отзыв на автореферат 2.pdf

Отзыв на автореферат 3.pdf

Отзыв на автореферат 4.pdf

Отзыв на автореферат 5.pdf

Отзыв на автореферат.pdf

Отзыв научного руководителя.pdf

Отзыв официального оппонента 2.pdf

Отзыв официального оппонента.pdf

Прочти меня!!!.txt

Сведения о ведущей организации.pdf

Сведения о результатах публичной защиты.pdf

Поделитесь ссылкой:

Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.

Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.

Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.

Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.

Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.

Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.

Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.

Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.

Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.

Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.

Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.

Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.