Отзыв официального оппонента 2 (Трассирующая нормализация)

официального оппонента на диссертационную работу Березуна Даниила Андреевича на тему «Трассирующая нормализация», представленную на соискание ученой степени кандидата физико-математических наук по специальности 05Л3.11 «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей» Диссертация отнес>пся к вьгуаг»,ио»у |ширавлсник»соре|и юской иифоршпики и прог!за>>пирования лячбла-испюлению. которое |арекочснловало себя кш >ффск|ивный шпон|пи |еский аппаргп лля чоле>шровапня и оптимизации кочпькпериых про|рачч.

В рабою исследована ироолсма иорчашшцни лямбла-тсрмов простого зниизпрованиа-о лях>г>.п>-исчисления. рассчозрши и,п|ислитс.п,иая сграшпш голошюй линейной рслукции, основанная на пг>дхолс трассир>к>шей норыаш|шшш Данный иолжл по>кот испольювпься в различных актуальных облас|ях. в иаспюсги в ои»шизации вьшис.|опий. авто»агитации построения доказательсш теорем.

и пру| их об>ластах. Автор исслсдус>. открьпый вопрос раапирсння |юля»да зр;ысируюп|ей норлш.в|анни |к> оси|с.|ения. иол>кно по 1ыориигу. 1> своей лискер|шиш ои обосновал корре|гпюс|| своего алгори|ча трассиру|шией нормали»мни для не|иии|ировшшого лячолв-ис шслспня. исс.|слова.| алаи;анни |расснруюпюй нормализации лля ра|,ш ни>х армс| ий вы шслсиий и ра|жчшрсл пр~..|стшшсипя ражи ншж языковых конструкций в рачках прсдто кснишо и|лхола при козин>ляпин фуикциона|п,иых языков прогрея>ыирования.

Кроче |ого. а|пор выио.ншл про| рвччную реяли юшин изложенных в,|иссср|ацни результа|ов, > аким о>>раз>зх>, налицо иаучиаи иовииш прсдс|авлсииого нсслсловаипя Основные ре>улыазы диссертации заключаются в следуюшеч, 1. Разрабо|аи алгор|пч грассир>юшей иорыализацш| „пя ис|и|ш|ирова|июго лячола-нешслсиия. соозвс|с|вуюший порча.шночу порялк| рот,к|иш. ', !!рсдс>явлена чо.|е.|ь по.шой | оловиой .шнсйн| й рого к|цш.

як.иннин>яся раси|прописи извес|ной >ц>>ели головной линсйша род>кции. 11релшпкенн:ш шмель форти>лицниии> в г|иле сис|е>и| порох»»ов.;юк»зава коррслгносзь >той модели относи гелыю | о.ювной рслуьцин 3. Докацию ьоррск | нос| ь прело |авлспиого а,и оршча трассирую|цсй норхиш>папин огнос|ие|и но предложенной чек|и иол|юй |оюаиоп линейной !>еду»ции |Отеч по фо1жи|лн|апии в ви>ю сне|с.|ы переходов и дальнейшей снчуляции сисгечы переходов лля полной | о кник>й линейной реги клип 4. 111>епло>кши|ый а и о!|и | и анап| проели:| |я:|рЗ | их.

«>ли пи |х от |юрия и ног о гк>ря>ка, с|вше| ий вычис.,|.'и!!: апп.шюп инно| и п«р>шка рс |укций и вышка |ю нсоохжшш>с>и 5. Предложен и реализован на примере ие>пши|иршю|шо|о лячола-ион»слепня иовьш че|ол кочиил>пши функциональных языков програчцирования в ни коуро>певце прелшавлеиис пу>бч спепиа|шюиш| представленного а:и оритчв трассиру|ошсй иорчализапии па вхолиой герч Данные резулшаты в ло.|жной сшиени ооосноваиы. нх ло>повер>к>сть пол|вержлена форчвльнычи локаштсльсгваии. а гакясе иилоп|ой про| рениной реалии|пей и зашя:риис|печи. Все рс>у:югпы рабов ы опубликованы в 5 пс |втиых работах.

из них лве едино,пшные с|во,и излаиы в журил>ш,, из "1!ерсння российских рецеишруеш |к иаучиьж жур|ы:|ош в ко|орьж лолжпы быть ог>!генно>вены ос|ювныс научные резулшазы диссертаций на оискаиие >левых ст«пеней доктора и канлилпа и|»к"..|кс статьи ои>бликоваиы в изданиях, вхоля|цих в базы |згзтировзния БС1>!|1'!э и Гусб оГ!|с|спеси Диссертация состоит из ввел«иия. шссп| г.шв, шкшо ьм|ия и лвэ:. приложсиий. 0бэь«з«э шссерзашш составляет ! )Л с|рации с З1 рисуикоч и 1 |аблицсй, !3 |лаве 1 автор иша|ает основные понятия бссги|ювого и |эрос||это язв|э|зэзрээвагзного лямбца-исиислеиия и приволит обзор сущестнуюп|их полхолов к нормализации лячбда-.|ерчов и к трассирунэшсй нормализации. Рассматрившотся сильная и слабая страгегии релукцш| лячбла-.|срмов. головная релукция.

и со«этвезствукээцззе им нормальные формы, а также соогвешц|экилис ич деревья Бема и абстрактные синтаксические лерсвья. 11аибш|се иолробио р|юсчатриваегчя |о некая .шлейная рсл«кцв| лямб:ш-шрлюв. автор локазывас| т«орем> о связи лячо:|а-з«)э«|а и )ш|«лата|а и!элис|миля к исм«|о:юв|кэй .и|лейлой редукции. а таклш усшиавлинает связь чсжл> |авсршасчошью |оловиои линейная релукции и |авершаемосгью головной рс» кции. Во второй глана автор ирелс|авляс| чолель полной |оловной:шлейной рс;1укции.

ко|орка яж|ясгся расширением мо |ели гкювиой линейной р«"»кции. пресы|оя|сниой >' !>апгэа и 1.. Кейп)ег. Автор привалит форлшльиос пре,|ставление обсох «згээгеэзсгй и лиле систем иерехолов и локазываез коррскзиосп обеих молслсй путем установления согласованности обои. чолслсй с |оловиои релукцисй лячбла-|ермов. Доказательство данного факта !шорема ') являася нстривпвальиым и исиоль»ст ивелси|юе авзороч понятие фуикции расширения с |р. которая ио сос|ояиию акиечы исрехолов вычис.|яс| соотв|ешп|уюи|ий ечу лямбла-герм, полу шсмый иоследова|ельиой рслэкиисй иссх |цюо|ы' ролексов.

иакопишии,ся в процессе лш|жсиия |ж ив шльио|о сос|ояиия. Слсдсп|иеч |еоречы ." являс|а»«|т фак|. иго го|к|виля линейная рел«кция завершается то|да и только т|нлп. котла завершает я | о ювиая рслукция Далее вволигся чолсль полной головной линейной рсл«кции, козорая яв.шс|ся расишрсиисм |оловиой лиисйиой рслукц|ш. рскурсивио причеишошич нос.ю шняо к ар| учс|пач ири юсгижсиии колечко|о сос|ояиия. Ав|ор ириволи| определение полной |оловиой льэиейиюй рсл|киии в вила шштемы псрсхо.юв.

явлшо|иийся расширеииеч системы переходов лля г|шовиой лиисриюй рсл,книи А|мор оооаювывает коррек|иошь по.|ной г«э.ювиой лииейиой рсяукции путе|э ишюльювшшя функции расширеиия (ехр) соаояиий системы перехолов „нэ созэтвегсгв>з«эщ«ио лямбла-герма, и л|и|азываш |сором> 1зеорсча э) о |ом. иго новая головная .шнсйиая релукшш завершается тоги и |олько тогда. ко|ха герч ия|есг порчалы»н фо!эму. р|ш|ш 3 |юсвяш«иа к.иоясвочу 1|«|>лыа|> л|юсс)э|шши - ишоэк«иикэ а.|мэрия ма |)эгзс«з|р>|ош«и нормализации ие|игшзироваиио|о |ичб|а-|ш|ишлсния. А.иоритм пол>и||от иа |зхгэл ироишош,иый лячб,атсрч.

и иорл|али|ужг шо |в том сзэ>иае, когла иорчалышя форча с«шсааэс|) 1!Роцелура иорэ|али мил|и является ||э|терна|э|взэй по огио|исиию л класашеским ир|иш«»раз| норма||ншш|и. осиоваииыч |ш ачсиах ползерчов, и вынолияе|ся |э>|ем оохо и а|эшракгного а|игаксичсслш о лсрева шрчш о«тавляя сач |ерч иси|меииьа. А|згор исиолыусз хвое|о-рскэрсивиыс ирсобра|ояания п>гсч |амок влгэязсиных вызовов семантической функции иа вылов лоиолиигсльиой ф>икиии прололэксиия и лсф>нкцгэгэээгзлиз|зцпи. Далее в преобразованиях исиолыуегся сечш||ика истшэрин и окруж«иий, иа основе ко|орой произволигся шчеиа окр>|кения из хвосзо-рекурсивной сема|цикл иа стр>шуру лш|иыч Заключите|и,иыч шаго«| трассирунэшсй иорчализации является преобразование окру|кения в историю вычислений, )лава завершасзся нримероч работы алгор|пма грасси!э>эогэзейз нормализации. Глава 4 посвяи|еиа обосиованикэ коррскпюстп алгоритча грассирую|пей норчализацни исп|п|ыировашю|о лямбла-исчислеиия.

Автор сначала рассчатривае| ограии или» кэ версикэ алнэрит«ш трассиру|ошей нормалэззацигз в визе сэзстсхэы исрехо |ов и >сзаиавшвас| сооз вше| кис м«экл««и«|с«эа«в псрсхо|ов л |я голов|э«эй линейной рсл>киии и ограииие|вой версии а|лори|ма |раею|рукиной иорчализации. опрслс,ииз фуикц|ио преобразования состояний о;и|ой системы пс!эехозг|э|э в сгэсэээяиээгэ,зр>э«эй. Зашч ав|ор устанавливает взаимно олиозиалиое соо|всзсншс эзсэкл> |оловиой лиисшюй ргшукцией и ограниченной версией алгоритма грассирую|пей порча:шшции ие|шшшрованиого лячбла-исчисления.

Автор лока|ынас| утвержлсиие !теор«ча Л] о коррскзиосп| алгори|ма в|эсгиаиоалснв| состоя|шя сис|емы и«рсхо кэв лля голою|ой линейной рел|кпии из соотве|дв>юшего со|яояш|я сис|счы переколов лля ограни ииинио алгоригма трассг~рукзцгсй игйзчалииигии. Зюсч авзгз1з лоюзиявггсг утке!ззюзсиис 1зсгзрсчв 5! сззгласозввшзйсги а,ло1зигча г!звсси!зыоизсй ио!зчгсггйа~!ии исзглшги!зогза~иклз~ лямгз.гачгс иге ~сгшя с игьлюй головной линейной рсдзкиисй, слало~вием коюрого являсшя 5 ~вержлшшс о гюго!зшасмости алгоритма трассируюшей норзгализаггии в тоз~ и только том сл5 иве.