Как найти лямбда общее

Обновлено: 24.05.2023

Начнём мы с традиционного (но краткого) экскурса в историю. В 30-х годах прошлого века перед математиками встала так называемая проблема разрешения (Entscheidungsproblem), сформулированная Давидом Гильбертом. Суть её в том, что вот есть у нас некий формальный язык, на котором можно написать какое-либо утверждение. Существует ли алгоритм, за конечное число шагов определяющий его истинность или ложность? Ответ был найден двумя великими учёными того времени Алонзо Чёрчем и Аланом Тьюрингом. Они показали (первый — с помощью изобретённого им λ-исчисления, а второй — теории машины Тьюринга), что для арифметики такого алгоритма не существует в принципе, т.е. Entscheidungsproblem в общем случае неразрешима.

Так лямбда-исчисление впервые громко заявило о себе, но ещё пару десятков лет продолжало быть достоянием математической логики. Пока в середине 60-х Питер Ландин не отметил, что сложный язык программирования проще изучать, сформулировав его ядро в виде небольшого базового исчисления, выражающего самые существенные механизмы языка и дополненного набором удобных производных форм, поведение которых можно выразить путем перевода на язык базового исчисления. В качестве такой основы Ландин использовал лямбда-исчисление Чёрча. И всё заверте…

λ-исчисление: основные понятия

Синтаксис

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

Мы с вами рассмотрим его наиболее простую форму: чистое нетипизированное лямбда-исчисление, и вот что конкретно будет в нашем распоряжении.

Термы:

переменная: x
лямбда-абстракция (анонимная функция): λx.t , где x — аргумент функции, t — её тело.
применение функции (аппликация): f x , где f — функция, x — подставляемое в неё значение аргумента
  • Применение функции левоассоциативно. Т.е. s t u — это тоже самое, что (s t) u
  • Аппликация (применение или вызов функции по отношению к заданному значению) забирает себе всё, до чего дотянется. Т.е. λx. λy. x y x означает то же самое, что λx. (λy. ((x y) x))
  • Скобки явно указывают группировку действий.
Процесс вычисления

Рассмотрим следующий терм-применение:

Существует несколько стратегий выбора редекса для очередного шага вычисления. Рассматривать их мы будем на примере следующего терма:

который для простоты можно переписать как

(напомним, что id — это функция тождества вида λx.x )

В этом терме содержится три редекса:

Недостатком стратегии вызова по значению является то, что она может зациклиться и не найти существующее нормальное значение терма. Рассмотрим для примера выражение

(λx.λy. x) z ((λx.x x)(λx.x x))

Ещё одна тонкость связана с именованием переменных. Например, терм (λx.λy.x)y после подстановки вычислится в λy.y . Т.е. из-за совпадения имён переменных мы получим функцию тождества там, где её изначально не предполагалось. Действительно, назови мы локальную переменную не y , а z — первоначальный терм имел бы вид (λx.λz.x)y и после редукции выглядел бы как λz.y . Для исключения неоднозначностей такого рода надо чётко отслеживать, чтобы все свободные переменные из начального терма после подстановки оставались свободными. С этой целью используют α-конверсию — переименование переменной в абстракции с целью исключения конфликтов имён.

Так же бывает, что у нас есть абстракция λx.t x , причём x свободных вхождений в тело t не имеет. В этом случае данное выражение будет эквивалентно просто t . Такое преобразование называется η-конверсией.

На этом закончим вводную в лямбда-исчисление. В следующей статье мы займёмся тем, ради чего всё и затевалось: программированием на λ-исчислении.

Как уже говорилось ранее, в чистом бестиповом лямбда-исчислении отсутствует всё, кроме функций. Так что даже такие элементарные вещи, как числа или булевы значения необходимо реализовывать самим. Точнее, надо создать некие активные сущности, которые будут вести себя подобно необходимым нам объектам. И, естественно, процесс кодирования будет заключаться в написании соответствующих функций.

Начнём мы с самого простого: True и False . Два терма, воплощающие поведение этих констант, выглядят следующим образом:

tru = λt.λf.t Двухаргументная функция, всегда возвращающая первый аргумент
fls = λt.λf.f Двухаргументная функция, всегда возвращающая второй аргумент

Оператор if под такие булевы константы будет имеет вид:
if = λb. λx. λy.b x y
Здесь b — tru или fls , x — ветка then , y — ветка else .

Посмотрим, как это будет работать:
if fls t e

Поскольку условие if ложно ( fls ), то должно возвращаться выражение из ветки else ( e в нашем случае).

(λb. λx. λy. b x y) fls t e по определению if
(λx. λy. fls x y) t e редукция подчёркнутого выражения из предыдущей строки
(λy. fls t y) e редукция подчёркнутого выражения из предыдущей строки
fls t e редукция подчёркнутого выражения из предыдущей строки
(λt.λf. f) t e по определению fls
(λf. f) e редукция подчёркнутого выражения из предыдущей строки
e редукция подчёркнутого выражения из предыдущей строки

or = λx.λy. x tru y

not = λx. x fls tru

Числа Чёрча

Мы с вами будем кодировать только натуральные числа, для чего вспомним аксиомы Пеано, определяющие их множество. В основе реализации по-прежнему будут лежать функции, ведущие себя в заданном контексте подобно единице, двойке и т.д. Собственно, это одна из особенностей лямбда-исчисления: сущности, записанные в его терминах, не обладают самодостаточностью, поскольку воплощают поведение того или иного объекта.

Итак, нам нужна функция, принимающая два аргумента: фиксированное начальное значение и функцию для определения следующего элемента (функцию следования). Число будет закодировано в количестве применений функции следования к начальному значению:

0 ≡ λs.λz. z функция s применяется к начальному значению z нуль раз
1 ≡ λs.λz. s z функция s применяется к начальному значению z один раз
2 ≡ λs.λz. s (s z) функция s применяется к начальному значению z два раза
. и так далее

Легко заметить, что нуль кодируется так же, как и логическое False. Тем не менее, не стоит делать из этого какие-либо далеко идущие выводы: это всего лишь совпадение.

Задача функции следования состоит в том, чтобы прибавить к заданному числу единицу. Т.е. в качестве аргумента она будет принимать значение, которое требуется увеличить, и которое тоже является функцией двух аргументов. Таким образом, суммарно функция (+1) имеет три аргумента: предшествующее число Чёрча n , функцию, которую надо будет применить n+1 раз к начальному значению, и само начальное значение. Выглядит это так:
scc = λn. λs. λz. s (n s z)
Здесь n s z — n раз применённая к z функция s . Но нам нужно применить её n+1 раз, откуда и берётся явное s (n s z) .

Арифметические операции

Сложение

Функция, осуществляющая сложение двух чисел Чёрча, будет принимать два слагаемых: x и y , которые в свою очередь тоже имеют по два аргумента — s (функцию следования) и z (начальное значение). Сложение будет состоять в том, чтобы сначала применить s к z x раз, а потом ещё y раз.

plus = λx. λy. λs. λz. x s (y s z)

В качестве примера сложим one = λs.λz. s z и two = λs.λz. s (s z) . Ответ должен будет выглядеть так: three = λs.λz. s (s (s z)) .

plus one two s’ z’ s’ и z’ — чтобы не путать подставляемые значения с именами переменных
(λx. λy. λs. λz. x s (y s z)) one two s’ z’ по определению plus
one s’ (two s’ z’) после проведения редукции
(λs.λz. s z) s’ (two s’ z’) по определению one
s’ (two s’ z’) после проведения редукции
s’ (( λs.λz. s (s z) s’ z’) по определению two
s’ (s’ (s’ z’)) после проведения редукции
three s’ z’ по определению three
Умножение

Функцию для умножения можно определить через функцию сложения. В конце-концов, умножить x на y означает сложить x копий y .

times = λx. λy. x (plus y) z

Есть ещё один способ определения умножения на числах Чёрча, без использования plus . Его идея заключается в том, что для получения произведения x и y нужно x раз взять y раз применённую к начальному значению функцию s :

times’ = λx.λy.λs.λz. x (y s) z

Для примера умножим two = λs.λz. s (s z) на three = λs.λz. s (s (s z)) . Результат должен будет иметь вид: six = λs.λz. s (s (s (s (s (s z))))) .

times’ two three s’ z’ s’ и z’ — чтобы не путать подставляемые значения с именами переменных
(λx.λy.λs.λz. x (y s) z) two three s’ z’ по определению times’
two (three s’) z’ после проведения редукции
(λs.λz. s (s z)) (three s’) z’ по определению two
three s’ ((three s’) z’) после проведения редукции
(λs.λz. s (s (s z))) s’ ((three s’) z’) по определению three
s’ (s’ (s’ ((three s’) z’))) после проведения редукции
s’ (s’ (s’ (((λs.λz. s (s (s z))) s’) z’))) по определению three
s’ (s’ (s’ (( (λz. s’ (s’ (s’ z))) z’ ))) после проведения редукции
s’ (s’ (s’ (s’ (s’ (s’ z’))))) редукция подчёркнутого выражения
six s’ z’ по определению six

Определите терм для возведения числа в степень

Для x в степени y :

power = λx.λy.λs.λz . y x s z

Заключение

Как видим, технически ничего сложного в лямбда-исчислении нет: всё сводится к элементарным подстановкам и редукциям. Но столь малого набора инструментов вполне хватает, чтобы при желании реализовать активные сущности, ведущие себя подобно парам, спискам, рекурсивным функциям и т.п. Они будут достаточно громоздкими, но, как уже говорилось, λ-исчисление предназначено не для написания программ, а для исследования и спецификации языков программирования и систем типов. С чем, собственно, и прекрасно справляется.

в интернете кто-то неправ

В очередном опусе Итана Сигеля резанула фраза

Пронаблюдав за удалёнными сверхновыми и измерив, как Вселенная расширялась миллиарды лет, астрономы обнаружили нечто удивительное, загадочное и неожиданное.

By observing distant supernovae and measuring how the Universe had expanded over billions of years, astronomers discovered something remarkable, puzzling and entirely unexpected

О какой неожиданности может идти речь? Там ведь совершенно шикарная история длиной в 80 лет с яркими открытиями и закрытиями. История про то, как на самом деле делается настоящая наука. История скорее про физиков, чем про физику.

О чём вообще весь сыр-бор?

Первую версию Общей Теории Относительности (ОТО) Альберт Эйнштейн представил публике 25 ноября 1915 года. В оригинале уравнения ОТО Эйнштейна выглядели вот так:

или, в современной записи, вот так:

Для неумеющего в тензоры читателя понятнее уравнение (1) в оригинальной записи Эйнштейна. Там написано, что энергия-импульс материи G равен кривизне пространства R плюс тензор Риччи S. (Этот самый тензор Риччи тоже есть кривизна, только в более другой форме).
Сейчас, решая уравнение ОТО, энергию-импульс обычно считают известным, а ищут как раз кривизну. Поэтому в современной записи стороны уравнения поменяли местами. Заодно поменяли буковки: G → T, S → Rμν.

Откуда есть пошла лямбда

Но физика — это вам не математика. Здесь нельзя взять формулу и напихать в неё добавочных слагаемых просто так. Нужно иметь очень веские основания, и теоретические, и экспериментальные.

Хотя ниже вы увидите, насколько мало Эйнштейн знал о Вселенной в те годы, но тогда, в 1916, такие основания у него были. Альберт Германович точно знал, что звёзды не попадали друг на друга и совершенно не собираются этого делать в обозримом будущем. Однако, в ОТО-1915 было только притяжение, которое нужно было чем-то сбалансировать.

Первое физическое толкование смысла лямбды

В такой трактовке ненулевое значение Λ означает, что наша Вселенная искривлена сама по себе, в том числе и при отсутствии какой-либо гравитации. Ну, вот такой нам достался мир. Однако, большинство физиков в это не верят, и считают, что у наблюдаемого искривления должна быть какая-то внутренняя причина. Какая-то неведомая доселе фигня, которую можно открыть.

На сегодняшний день измеренная кривизна пространства Вселенной таки равна нулю, но с очень паршивой точностью, порядка 0.4%. И не очень-то видно способов эту точность улучшить.
С измерениями кривизны есть две концептуальные проблемы.

Первая в том, что мы не можем измерить совсем пустое пространство, потому что просто ничего там не видим. А если там есть что-то, что мы таки видим, то пространство уже не пустое и, значит, уже дополнительно искривлено гравитацией.

Допустим, у нас есть как-то измеренные координаты объектов, плюс пачка фотографий этих объектов в разных ракурсах (снятых из разных точек). Тогда мы можем вычислить кривизну пространства. Например, гравитация Солнца отклоняет пролетающий мимо свет далёких звёзд. Во время солнечных затмений это отклонение можно измерить экспериментально и сравнить с предсказаниями ОТО.

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

Поэтому измерить кривизну наблюдаемой Вселенной в целом мы можем только из очень окольных соображений.

Вселенная Фридмана

Meanwhile in Russia, не смотря на войны и революции, над теорией ОТО бился прапорщик (и по совместительству профессор) Александр Александрович Фридман. Он рассмотрел все варианты лямбд и выяснил следующее:

При Λ < 0 имеют место лишь силы притяжения, как гравитационные, так и вызванные кривизной впуклоговогнутого пространства. Рано или поздно звёзды и галактики в таком мире таки попадают друг на друга. Причём конец будет неожиданно быстрым и очень горячим.

Но самое интересное происходит при Λ = 0. Здесь всё зависит от начальных условий — т.е. координат и скоростей конкретных галактик. Возможны три варианта: большое сжатие, большой разлёт и стационарный вариант, когда галактики разлетаются, но с относительно небольшими скоростями и без ускорения.

Сегодня вышеописанные ситуации называются космологическими решениями Фридмана.

Статьи Фридмана 1922 и 1924 годов отменяли необходимость в лямбда-члене, из-за чего поначалу были приняты Эйнштейном в штыки.

За свою работу Фридман вполне мог претендовать на Нобелевку.

Летом 1925 он женился, поехал в свадебное путешествие в Крым, съел там немытую грушу, заразился тифом и в сентябре — умер.

И да, статья Итана про примерно такой график (конкретно на этом учтены данные на 2010 год):

Здесь по горизонтали отложено z — это красное смещение, по вертикали наблюдаемая яркость сверхновых особого типа Ia, которые всегда выделяют одно и то же количество энергии. Вообще, это два способа измерения одного и того же расстояния, но, так сказать, в разные моменты времени.

Серые палки — наблюдавшиеся события с их погрешностью измерений. Синим пунктиром отложено предсказание при Λ = 0, красной линией — аппроксимация фактически наблюдаемых значений. Отклонение красной линии от прямой означает, что Вселенная расширяется ускоренно. Но Эйнштейн об этом так и не узнал.

Вселенная Каптейна

Перейдём к экспериментальной части.

Голландский астроном Якобус Корнелиус Каптейн открыл звезду Каптейна в 1897, после чего приступил к opus magnum всей своей жизни. Объединяя огромное количество наблюдений разных обсерваторий, он попытался создать первую карту Вселенной. По его карте выходило, что вселенная имеет форму вращающегося (sic!) диска крышесносящего по тем временам размера 40000 световых лет, причём Солнце находится отнюдь не в центре, а вполне себе на задворках. Закончена и опубликована эта работа была только в 1922.

Для понимания уровня тогдашних знаний: то, что Каптейн считал невероятно огромной Вселенной, сегодня считается совершенно рядовой, ничем не примечательной среди миллиардов таких же… галактикой Млечный Путь. Тем не менее, заслуга Каптейна в том, что он открыл её вращение и приблизительно вычислил её центр.

Наблюдения Хаббла (астронома, а не телескопа)

Статью со своими открытиями, из которой следовало, что Вселенная значительно больше, чем наш Млечный путь, Хаббл представил американскому астрономическому обществу первого января 1925. За что и был освистан страдающими от похмелья коллегами, едва свыкшимися с расстояниями Каптейна.

Хаббл не унимался и прикрутил к телескопу ещё и спектрометр. Анализируя красное смещение галактик, он выяснил, что галактики разбегаются, а Вселенная, соответственно, расширяется. Заодно он открыл закон имени себя с константой имени себя (впрочем, закон был предсказан Леметром), и описал всё это в статьях к концу 20-ых годов. Согласно его наблюдениям, оказалась верна модель Фридмана для Λ = 0.

Это выбило из-под лямбды теперь уже и экспериментальные основания её существования.

Здесь ещё нужно упомянуть, что первоначальные оценки Хаббла были очень уж неточными и показывали возраст Вселенной порядка 2 миллиардов лет. Позднее это войдёт в противоречие с данными геофизиков, которые при помощи радиоизотопного анализа оценят возраст Земли в несколько миллиардов лет, и десятилетиями будет сильнейшей головной болью для физиков-космологов.

Стационарная Вселенная Хойла

С начала 30-ых годов вопрос с лямбдой считался решённым, и из мейнстримных физиков ей никто толком не занимался. Одним из редких исключений, рискнувших попереть супротив самого Эйнштейна, стал британец Фред Хойл.

Речь пойдёт о гелии. Этот элемент феноменально инертен и не хочет ни с чем реагировать. Причём не только химически, но и физически тоже, если мы говорим про гелий-4. Его ядро — альфа частица — имеет пиковую энергию связи на нуклон в своей области. см. рис из какого-то реферата:

Это значит, что альфа-частица не может присоединить дополнительные протоны или другую альфа-частицу иначе как случайно: это просто-напросто энергетически невыгодно. А в ядрах звёзд ничего кроме протонов и альфа-частиц и нет.

Возникал резонный вопрос: а откуда, собственно, взялись химические элементы тяжелее гелия?

Ближайшее ядро, в которое может превращаться гелий-4, это углерод-12. Но для этого нужно объединить три альфа-частицы.

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

Однако, по расчётам Хойла выходило, что при наличии такого уровня в три-альфа процессе наступает резонанс, и звёзды — красные гиганты производят достаточно много углерода для нашего существования.

Удивительно, но американцы решили провести небольшой эксперимент на своём ускорителе. И да — триумфально нашли нужный энергетический уровень на 7.65 МэВ, который физики-ядерщики всего мира почему-то проглядели во всех предыдущих экспериментах.

Сегодня такое возбуждённое состояние углерода-12, когда три альфа-частицы фактически выстраиваются по линии, называется хойловским. Соответствующая статья Хойла, Фаулера и супругов-астрономов Джефри и Маргерит Бёрбиджей является краеугольным камнем современных теорий звёздного нуклеосинтеза и настолько часто цитируется, что обозначается просто B²FH, без ссылок и расшифровок.

И — да, на сегодня это чуть ли не единственное известное успешное предсказание на основе антропного принципа.

Однако, из квантовых флуктуаций постоянно рождается новое вещество, причём так, что средняя плотность материи остаётся одинаковой. Расчёты показывают, что в одном кубическом километре пространства должен рождаться всего-навсего один протон раз в 300000 лет (а так же один электрон или что-то типа того для сохранения электрического заряда). Прекрасное число, чтобы исключить любую возможность какой-либо экспериментальной проверки!

Теория стационарной Вселенной серьёзно рассматривалась как альтернатива теории Большого Взрыва в 50-х и начале 60-х. Но экспериментальное открытие в 1964 году предсказанного ТББ реликтового излучения поставило на ней крест.

За статью B²FH дали Нобелевку. Но только Фаулеру, который распорядился провести десятидневный эксперимент. Ни супругам Бёрбиджам, проводившим длительные астрономические наблюдения и собственно написавшим статью, ни автору идеи Хойлу нобелевку не дали — за упорствование в космологической ереси.

Квантовая лямбда

Вернёмся к уравнению ОТО.

Слева (в современной записи) стоит кривизна пространства, сиречь гравитация по ОТО. Справа — тензор энергии-импульса. Под этим тензором стоит жутко сложный матан, но суть в следующем: там учтена вся-вся-вся материя Вселенной во всех видах и состояниях. И обычное вещество, и всякие хитрые частицы, и все виды излучений (кроме гравитации, которая слева).

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

Первая гипотеза состоит в том, что лямбда — это энергия собственно вакуума. Звучит диковато, но на самом деле вполне согласуется с квантовой механикой. Возьмём кусок пространства и уберём из него всё, что хотя бы в принципе можно убрать. Уберём всё вещество, все частицы и все волны, независимо от их природы. Останутся только физические поля в невозмущённом состоянии. Полный штиль.

Так вот, у некоторых полей (например, Хиггсовских) в пустоте ненулевое значение. И теоретически у них есть некоторая энергия. Кроме того, в силу принципа неопределённости у любых полей есть квантовые флуктуации — и они тоже имеют некоторую энергию.

Вместо заключения

Лямбда-исчисление — это формальная система в математической логике для выражения подсчетов на основе абстракции и применения функций с использованием привязки и подстановки переменных. Это универсальная модель, которую можно применять для проектирования любой машины Тьюринга. Впервые введена лямбда-исчисления Черчем, известным математиком, в 1930-х годах.

Система состоит из построения лямбда-членов и выполнения над ними операций сокращения.

Пояснения и приложения

лямбда исчисление решения

Греческая буква lambda (λ) используется в лямбда-выражениях и лямбда-терминах для обозначения связывания переменной в функции.

Лямбда-исчисление может быть нетипизировано или типизировано. В первом варианте функции могут быть применены только в том случае, если они способны принимать данные этого типа. Типизированные лямбда-исчисления слабее, могут выражать меньшее значение. Но, с другой стороны, они позволяют доказывать больше вещей.

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

Система находит применение во многих различных областях математики, философии, лингвистики, и компьютерных наук. В первую очередь, лямбда-исчисления — это расчет, который сыграл важную роль в развитии теории языков программирования. Именно стили функционального создания реализуют системы. Они также являются актуальной темой исследований в теории этих категорий.

Для чайников

Лямбда-исчисление была введена математиком Алонзо Черчем в 1930-х годах в рамках исследования основ науки. Первоначальная система была показана как логически несовместимая в 1935 году, когда Стивен Клин и Дж. Б. Россер разработали парадокс Клини-Россера.

В последствии, в 1936 году Черч выделил и опубликовал только ту часть, которая имеет отношение к расчетам, то, что сейчас называется нетипизированным лямбда-исчислением. В 1940 он также представил более слабую, но логически непротиворечивую теорию, известную как система простого типа. В свое работе он объясняет всю теорию простым языком, поэтому, можно сказать, что Черч опубликовал лямбду исчисления для чайников.

До 1960-х годов, когда выяснилось его отношение к языкам программирования, λ стала лишь формализмом. Благодаря применениям Ричарда Монтегю и других лингвистов в семантике естественного языка, исчисление стало занимать почетное место как в лингвистике, так и в информатике.

Происхождение символа

лямбда исчисление

Введение в лямбда исчисление

примеры решения

Система состоит из языка терминов, которые выбираются определенным формальным синтаксисом, и набора правил преобразования, которые позволяют манипулировать ими. Последний пункт можно рассматривать как эквациональную теорию или как операционное определение.

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

Лямбда-термины

Следующие три правила дают индуктивное определение, которое можно применять для построения всех синтаксически допустимых понятий:

Переменная x сама по себе является действительным лямбда-термином:

  • если T это ЛТ, и x непостоянная, то (lambda xt) называется абстракцией.
  • если T, а также s понятия, то (TS) называется приложением.

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

Определение

лямбда исчисление примеры

Лямбда-выражения состоят из:

  • переменных v 1, v 2. v n.
  • символов абстракции ‘λ’ и точки ‘.’
  • скобок ().

Множество Λ, может быть определено индуктивно:

  • Если x переменная, то x ∈ Λ;
  • x непостоянная и M ∈ Λ, то (λx.M) ∈ Λ;
  • M, N ∈ Λ, то (MN) ∈ Λ.

Обозначение

Чтобы сохранить нотацию лямбда-выражений в незагроможденном виде, обычно применяются следующие соглашения:

  • Внешние скобки опущены: MN вместо (MN).
  • Предполагается, что приложения остаются ассоциативными: взамен ((MN) P) можно написать MNP.
  • Тело абстракции простирается дальше вправо: λx.MN означает λx. (MN), а не (λx.M) N.
  • Сокращается последовательность абстракций: λx.λy.λz.N можно λxyz.N.

Свободные и связанные переменные

Оператор λ соединяет свою непостоянную, где бы он ни находился в теле абстракции. Переменные, попадающие в область, называются связанными. В выражении λ x. М, часть λ х часто называют связующим. Как бы намекая, что переменные становятся группой с добавлением Х х к М. Все остальные неустойчивые называются свободными.

Множество свободных переменных M обозначается как FV (M) и определяется рекурсией по структуре терминов следующим образом:

  • FV (x) = , где x — переменная.
  • FV (λx.M) = FV (M) .
  • FV (MN) = FV (M) ∪ FV (N).

Формула, которая не содержит свободных переменных, называется закрытой. Замкнутые лямбда-выражения также известны как комбинаторы и эквивалентны терминам в комбинаторной логике.

Сокращение

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

Существует три вида урезания:

  • α-преобразование: изменение связанных переменных (альфа).
  • β-редукция: применение функций к своим аргументам (бета).
  • η-преобразование: охватывает понятие экстенсиональности.

Здесь речь также идет о полученных эквивалентностях: два выражения являются β-эквивалентными, если они могут быть β-преобразованы в одно и то же составляющее, а α / η-эквивалентность определяется аналогично.

Термин redex, сокращение от приводимого оборота, относится к подтемам, которые могут быть сокращены одним из правил. Лямбда исчисление для чайников, примеры:

(λ x.M) N является бета-редексом в выражении замены N на x в M. Составляющее, к которому сводится редекс, называется его редуктом. Редукция (λ x.M) N есть M [x: = N].

Если x не является свободной в M, λ х. М х также ет-REDEX с регулятором М.

α-преобразование

Альфа-переименования позволяют изменять имена связанных переменных. Например, λ x. х может дать λ у. у. Термины, которые отличаются только альфа-преобразованием, называются α-эквивалентными. Часто при использовании лямбда-исчисления α-эквивалентные считаются взаимными.

Точные правила для альфа-преобразования не совсем тривиальны. Во-первых, при данной абстракции переименовываются только те переменные, которые связаны с одной и той же системой. Например, альфа-преобразование λ x.λ x. x может привести к λ y.λ x. х, но это может не ввергнуть к λy.λx.y Последний имеет иной смысл, чем оригинал. Это аналогично понятию программирования затенения переменных.

Во-вторых, альфа-преобразование невозможно, если оно приведет к захвату непостоянной другой абстракцией. Например, если заменить x на y в λ x.λ y. x, то можно получить λ y.λ y. у, что совсем не то же самое.

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

В нотации индекса Де Брюйна любые два альфа-эквивалентных термина синтаксически идентичны.

Замена

Изменения, написанные Е [V: = R], представляют собой процесс замещения всех свободных вхождений переменной V в выражении Е с оборотом R. Подстановка в терминах λ определяется лямбдой исчисления рекурсии по структуре понятий следующим образом (примечание: x и y — только переменные, а M и N — любое λ-выражение).

y [x: = N] ≡ y, если x ≠ y

(M 1 M 2) [x: = N] ≡ (M 1 [x: = N]) (M 2 [x: = N])

(λ x.M) [x: = N] ≡ λ x.M

(λ y.M) [x: = N] y λ y. (M [x: = N]), если x ≠ y, при условии, что y ∉ FV (N).

Для подстановки в лямбда-абстракцию иногда необходимо α-преобразовать выражение. Например, неверно, чтобы (λ x. Y) [y: = x] приводило к (λ x. X), потому что замещенный x должен был быть свободным, но в итоге был связанным. Правильная замена в этом случае (λ z. X) с точностью до α-эквивалентности. Стоит обратить внимание, что замещение определяется однозначно с верностью до лямбды.

β-редукция

Бета-редукция отражает идею применения функции. Бета-восстановительный определяется в терминах замещения: ((X V. E) Е ‘) является Е [V: = Е’].

Например, предполагая некоторое кодирование 2, 7, ×, имеется следующее β-уменьшение: ((λ n. N × 2) 7) → 7 × 2.

Бета-редукция может рассматриваться как то же самое, что и концепция локальной сводимости при естественной дедукции через изоморфизм Карри – Ховарда.

η-преобразование

лямбда примеры задач

Эта-конверсия выражает идею экстенсиональности, которая в этом контексте заключается в том, что две функции равны тогда, когда они дают одинаковый результат для всех аргументов. Эта конвертация обменивает между λ x. (F x) и f всякий раз, когда x не кажется свободным в f.

Данное действие может рассматриваться как то же самое, что и концепция локальной полноты в естественной дедукции через изоморфизм Карри – Ховарда.

Нормальные формы и слияние

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

Тем не менее можно показать, что β-редукция сливается при работе до α-преобразования (т. е. можно считать две нормальные формы равными, если возможно α-преобразование одной в другую).

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

Дополнительные методы программирования

лямбда виды решения

Существует большое количество идиом создания для лямбда-исчисления. Многие из них были первоначально разработаны в контексте использования систем в качестве основы для семантики языка программирования, эффективно применяя их в качестве создания низкого уровня. Поскольку некоторые стили включают лямбда-исчисление (или что-то очень похожее) в качестве фрагмента, эти методы также находят применение в практическом создании, но затем могут восприниматься как неясные или чужие.

Именованные константы

В лямбда-исчислении библиотека принимает форму набора ранее определенных функций, в которой термины являются просто конкретными константами. Чистое исчисление не имеет понятия именованных неизменных, поскольку все атомные лямбда-термины являются переменными. Но их также можно имитировать, выделив непостоянную в качестве имени константы, используя лямбда-абстракцию для связывания этой изменчивой в основной части, и применить эту абстракцию к намеченному определению. Таким образом, если использовать f для обозначения M в N, можно сказать,

Авторы часто вводят синтаксическое понятие, такое как let, чтобы разрешить писать все в более интуитивном порядке.

Заметным ограничением этого let является то, что имя f не определено в M, поскольку M находится вне области привязки лямбда-абстракции f. Это означает, что атрибут рекурсивной функции не может использоваться как M с let. Более продвинутая синтаксическая конструкция letrec, которая позволяет писать рекурсивные определения функций в этом стиле, вместо этого дополнительно использует комбинаторы с фиксированной точкой.

Печатные аналоги

лямбда решения

Данный тип является типизированным формализмом, который использует символ для обозначения анонимной функции абстракция. В этом контексте типы обычно являются объектами синтаксической природы, которые присваиваются лямбда-терминам. Точная натура зависит от рассматриваемого исчисления. С определенной точки зрения, типизированные ЛИ можно рассматривать как уточнения нетипизированного ЛИ. Но с другой стороны, их также можно считать более фундаментальной теорией, а нетипизированное лямбда-исчисление — особым случаем только с одним типом.

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

Типизированные лямбда-исчисления тесно связаны с математической логикой и теорией доказательств через изоморфизм Карри – Говарда, и их можно рассматривать как внутренний язык классов категорий, например, который просто является стилем декартовых замкнутых.

Обобщим некоторые сведения о векторах, известные в основном из школьного курса геометрии.

Вектором называется направленный отрезок с начальной точкой А и конечной точкой В (который можно перемещать параллельно самому себе.

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

Длиной (или модулем) вектора называется число, равное длине отрезка АВ, изображающего вектор.

Векторы, лежащие на одной прямой или на параллельных прямых, называются коллинеарными (параллельными).

Если начало и конец вектора совпадают, например, , то такой вектор называют нулевым и обозначают .

Длина нулевого вектора равна нулю. Так как направление нулевого вектора произвольно, то считают, что он коллинеарен (параллелен) любому вектору.

Произведением вектора на число (лямбда) называется вектор , имеющий длину , направление которого совпадает с направлением вектора , если , и противоположно ему, если .

Противоположным вектором называется произведение вектора на число (-1).

Суммой двух векторов и называется вектор , начало которого совпадает с началом вектора , а конец – с концом вектора при условии, что начало вектора совпадает с концом вектора (правило треугольников).

Аналогично определяется сумма нескольких векторов. Так, например, сумма четырех векторов (рис. а) есть вектор , начало которого совпадает с началом вектора , а конец – с концом вектора (правило многоугольника) (рис. б).

Разностью двух векторов и называется сумма вектора и вектора , противоположного .

Легко убедиться в том, что в параллелограмме, построенном на векторах и , одна диагональ – вектор – представляет сумму векторов и , а другая диагональ — вектор – их разность.

Перенесем вектор параллельно самому себе так, чтобы его начало совпало с началом координат.

Координатами вектора называются координаты его конечной точки.

Так, координатами вектора на плоскости Оxy являются

два числа x и y: ,

а в пространстве Oxyz три числа x, y и z: .

Для векторов и , заданных координатами,

сумма определяется по формуле

разность – по формуле

произведение вектора на число λ – по формуле

.

Длина вектора равна корню квадратному из суммы квадратов его координат:

.

Если A(a1, a2, a3) — начало вектора, B(b1, b2, b3) — его конец, то

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

.

Из данного выражения можно найти косинус: .

Если векторы выражены через координаты в декартовой системе координат , , то скалярное произведение определяется как сумма попарных произведений соответствующих координат

.

Условием перпендикулярности векторов является равенство нулю их скалярного произведения .

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

;

.

Модуль вектора можно представить в виде .

Читайте также:

      

  • Какие кондиционеры ставят на гранту
  •   

  • 4 дроссельный впуск на ваз как установить
  •   

  • Как отличить бош от киржача ваз 2110
  •   

  • Парктроник рено каптур не работает
  •   

  • Какие подушки двигателя лучше поставить на ваз 2114

Найдите общее решение линейной системы в зависимости от значения параметра . При каких значениях система допускает решение с помощью обратной матрицы?

тогда систему можно записать в виде .

Приравнивая к нулю, найдем, что при и .

Если и , то матрица имеет обратную

и решение имеет вид .

Если аккуратно перемножить и упростить, получим .

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

Можно не использовать обратную матрицу, а применить метод редукции гаусса к расширенной матрице, учитывая, что и ,

При расширенная матрица

Следовательно решения имеют вид , или в матричном виде:

Теорема Кронекера-Капелли. Исследование систем линейных уравнений на совместность. Вторая часть.

В первой части мы рассматривали системы линейных алгебраических уравнений (СЛАУ), все коэффициенты которых были известны. В этой же части разберём СЛАУ, среди коэффициентов которых есть некий параметр. Для исследования СЛАУ на совместность станем использовать теорему Кронекера-Капелли. В процессе решения примеров на данной странице будем применять метод Гаусса или же метод Крамера. Сформулируем теорему и следствие из неё ещё раз:

Система линейных алгебраических уравнений совместна тогда и только тогда, когда ранг матрицы системы равен рангу расширенной матрицы системы, т.е. $rang A=rangwidetilde$.

Следствие из теоремы Кронекера-Капелли

Параметр $n$, использованный выше, равен количеству переменных рассматриваемой СЛАУ.

Исследовать СЛАУ $ left <begin& kx_1+2x_2+x_3=8;\ & -x_1+x_2+2x_3=7;\ & x_2+kx_3=5.endright.$ на совместность и найти решение системы в зависимости от значений параметра $k$.

Чтобы исследовать заданную систему на совместность, нам нужно найти ранг матрицы системы $A$ и ранг расширенной матрицы системы $widetilde$. Сделать это можно несколькими путями. Стоит учесть, что в данном примере нам требуется не только исследовать систему на совместность, но и указать её решения. Мне кажется наиболее удобным в таких задачах применять метод Гаусса, однако это вовсе не является обязательным. Для разнообразия данный пример решим методом Гаусса, а следующий – методом Крамера. Итак, запишем и начнём преобразовывать расширенную матрицу системы. При записи расширенной матрицы системы поменяем местами первую и вторую строки. Это нужно для того, чтобы первым элементом первой строки стало число -1.

$$ left(begin -1 & 1 &2 &7 \ k & 2 & 1 & 8\ 0 & 1 & k & 5 end right) begin phantom <0>\ r_2+kcdot\ phantom<0>endrightarrow left(begin -1 & 1 &2 &7 \ 0 & 2+k & 1+2k & 8+7k\ 0 & 1 & k & 5 end right)rightarrowleft|begin&text<меняем местами>\&text<вторую и третью строки>endright|rightarrow \ rightarrow left(begin -1 & 1 &2 &7 \0 & 1 & k & 5 \ 0 & 2+k & 1+2k & 8+7k end right) begin phantom<0>\phantom<0>\r_3-(2+k)cdotend rightarrow left(begin -1 & 1 &2 &7 \0 & 1 & k & 5 \ 0 & 0 & 1-k^2 & 2k-2 end right) $$

Мы привели расширенную матрицу системы к ступенчатому виду. Напомню, что до черты расположена преобразованная матрица матрица системы: $left(begin-1 & 1 &2\0 & 1 & k\ 0 & 0 & 1-k^2end right)$.

Каким бы ни было значение параметра $k$, полученная нами после преобразований матрица будет содержать не менее двух ненулевых строк (первая и вторая строки точно останутся ненулевыми). Вопрос о количестве решений зависит лишь от третьей строки.

В следствии из теоремы Кронекера-Капелли указаны три случая, и в данном примере легко рассмотреть каждый из них. Начнём с варианта $rang Aneqrangwidetilde$, при котором система не имеет решений, т.е. несовместна.

$rang Aneqrangwidetilde$

Ранги будут не равны друг другу лишь в одном случае: когда $1-k^2=0$, при этом $2k-2neq<0>$. В этом случае преобразованная матрица системы будет содержать две ненулевых строки (т.е. $rang A=2$), а преобразованная расширенная матрица системы будет содержать три ненулевых строки (т.е. $rang widetilde=3$). Иными словами, нам требуется решить систему уравнений:

Из первого уравнения имеем: $k=1$ или $k=-1$, однако $kneq<1>$, поэтому остаётся лишь один случай: $k=-1$. Следовательно, при $k=-1$ система не имеет решений.

$rang A=rangwidetilde<3$

Рассмотрим второй пункт следствия из теоремы Кронекера-Капелли – ранги равны между собой, но меньше, чем количество переменных (т.е. меньше 3). Это возможно лишь в том случае, если последняя строка преобразованной расширенной матрицы системы полностью станет нулевой, т.е.

Из данной системы имеем: $k=1$. Именно при $k=1$ третья строка преобразованной расширенной матрицы системы станет нулевой, поэтому $rang=rangwidetilde=2$. При этом, повторюсь, у нас всего три переменных, т.е. имеем случай $rang A=rangwidetilde=2<3$.

Система имеет бесконечное количество решений. Найдём эти решения. Подставим $k=1$ в преобразованную матрицу и продолжим операции метода Гаусса. Третью строку (она станет нулевой) просто вычеркнем:

$$ left(begin -1 & 1 &2 &7 \0 & 1 & k & 5 \ 0 & 0 & 1-k^2 & 2k-2 end right)rightarrow|k=1|rightarrow left(begin -1 & 1 &2 &7 \0 & 1 & 1 & 5 end right) rightarrowleft|begin&text<переносим третий столбец>\&text<за черту>endright|rightarrow \ rightarrowleft(begin-1 & 1 &-2 &7\0 & 1 & -1 & 5endright) begin r_1-r_2\phantom<0>end rightarrowleft(begin-1 & 0 &-1 &2\0 & 1 & -1 & 5endright) begin -1cdot\phantom<0>end rightarrowleft(begin1 & 0 &1 &-2\0 & 1 & -1 & 5endright) $$

$rang A=rangwidetilde=3$

Рассмотрим третий пункт следствия из теоремы Кронекера-Капелли – ранги равны между собой и равны количеству переменных. Это возможно лишь в том случае, если $1-k^2neq<0>$, т.е. $kneq<-1>$ и $kneq<1>$. Продолжаем решение методом Гаусса:

$$ left(begin -1 & 1 &2 &7 \0 & 1 & k & 5 \ 0 & 0 & 1-k^2 & 2k-2 endright)rightarrow left(begin -1 & 1 &2 &7 \0 & 1 & k & 5 \ 0 & 0 & (1-k)(1+k) & -2(1-k) endright) begin phantom<0>\phantom<0>\r_3:((1-k)(1+k))end rightarrow\ rightarrowleft(begin -1 & 1 &2 &7 \0 & 1 & k & 5 \ 0 & 0 & 1 & -2/(1+k) endright) begin r_1-2r_3\r_2-kcdot\phantom<0>end rightarrow left(begin -1 & 1 &0 &(7k+11)/(k+1) \0 & 1 & 0 & (7k+5)/(k+1) \ 0 & 0 & 1 & -2/(1+k) endright) begin r_1-r_2\phantom<0>\phantom<0>endrightarrow\ rightarrow left(begin -1 & 0 &0 &6/(k+1)\0 & 1 & 0 & (7k+5)/(k+1) \ 0 & 0 & 1 & -2/(1+k) endright) begin -1cdot\phantom<0>\phantom<0>endrightarrow left(begin 1 & 0 &0 &-6/(k+1)\0 & 1 & 0 & (7k+5)/(k+1) \ 0 & 0 & 1 & -2/(1+k) endright) $$

Исследовать СЛАУ $left <begin& 2kx_1+x_2+x_3=0;\ & x_1-x_2+kx_3=1;\ & (k-6)x_1+2x_2-4x_3=-3.endright.$ на совместность и найти решение системы при тех значениях параметра, при которых она совместна.

Вновь, как и в предыдущем примере, для того, чтобы исследовать заданную систему на совместность, нам нужно найти ранг матрицы системы $A$ и ранг расширенной матрицы системы $widetilde$. Чтобы исследовать систему на совместность и указать количество решений применим метод Крамера. Можно было бы решить и методом Гаусса, однако в предыдущем примере мы его уже использовали, поэтому для разнообразия решим задачу с помощью метода Крамера. Начнём с вычисления определителя матрицы системы. Этот определитель мы получим с помощью готовой формулы.

Значения переменных $x_1$, $x_2$, $x_3$ будут такими:

Нам остаётся исследовать совместность системы при условии $Delta=0$. Это равенство возможно при $k=0$ или $k=1$.

Случай $k=0$

Нам остаётся рассмотреть последний случай: $k=1$.

Случай $k=1$

Для наглядности я запишу здесь матрицу системы $A$ и расширенную матрицу системы $widetilde$, подставив $k=1$:

Если $k=1$, то $Delta=0$. Это значит, что $rang≤2$. Рассмотрим миноры второго порядка матрицы $A$. Например, возьмём минор, образованный на пересечении строк №1, №2 и столбцов №1, №2: $M=left|begin2 & 1\ 1 & -1endright|=-3$. Так как $Mneq<0>$, то ранг матрицы $A$ равен 2.

Задача решена, осталось лишь записать ответ.

Разберём ещё один пример, в котором рассмотрим СЛАУ с четырьмя уравнениями.

Исследовать СЛАУ $ left <begin& kx_1+x_2+x_3+x_4=1;\ & x_1+kx_2+x_3+x_4=1;\ & x_1+x_2+kx_3+x_4=1;\ & x_1+x_2+x_3+kx_4=1.endright.$ на совместность и найти решение системы в зависимости от значений параметра $k$.

Применим метод Гаусса. При записи расширенной матрицы системы поместим первую строку вниз, на место четвёртой строки. А дальше начнём стандартные операции метода Гаусса.

$$ left(begin 1 & k &1 &1&1 \ 1 & 1 &k &1&1 \ 1 & 1 &1 &k&1 \ k & 1 &1 &1&1 end right) begin phantom<0>\r_2-r_1\r_3-r_1\r_4-kcdotendrightarrow left(begin 1 & k &1 &1&1\ 0 & 1-k &k-1 &0&0\ 0 & 1-k &0&k-1&0\ 0 & 1-k^2 &1-k &1-k&1-kend right) $$

Здесь можно было бы остановиться и рассмотреть случаи $k=1$ и $kneq<1>$ отдельно. Цель таких действий: разделить вторую, третью и четвёртую строки на $k-1$ при условии $k-1neq<0>$. Однако пока что полученная нами матрица содержит не столь уж громоздкие элементы, поэтому сейчас отвлекаться на частности я не вижу смысла. Продолжим преобразования в общем виде:

$$ left(begin 1 & k &1 &1&1\ 0 & 1-k &k-1 &0&0\ 0 & 1-k &0&k-1&0\ 0 & 1-k^2 &1-k &1-k&1-kend right) begin phantom<0>\phantom<0>\r_3-r_2\r_4-(k+1)r_2endrightarrow \ rightarrow left(begin 1 & k &1 &1&1\ 0 & 1-k &k-1 &0&0\ 0 & 0 &1-k&k-1&0\ 0 & 0 &(1-k)(k+2) &1-k&1-kend right) begin phantom<0>\phantom<0>\phantom<0>\r_4-(k+2)r_3endrightarrow \ rightarrow left(begin 1 & k &1 &1&1\ 0 & 1-k &k-1 &0&0\ 0 & 0 &1-k&k-1&0\ 0 & 0 &0&(1-k)(k+3)&1-kend right) $$

Мы привели расширенную матрицу системы к ступенчатому виду. До черты расположена преобразованная матрица системы. Ранги матриц $A$ и $widetilde$ зависят от значения параметра $k$. Рассмотрим три случая: $k=1$, $k=-3$ и случай $kneq<1>$, $kneq<-3>$.

Случай $k=-3$

Случай $k=1$

Если $k=1$, то преобразованная матрица станет такой: $left(begin 1 & 1 &1 &1&1\ 0 & 0 &0 &0&0\ 0 & 0 &0&0&0\ 0 & 0 &0&0&0endright)$. Ранги матрицы системы и расширенной матрицы системы равны между собой (и равны 1), но меньше, чем количество переменных, т.е. $rang=rang<widetilde>=1<4$. Вывод: система является неопределённой. Общее решение системы непосредственно получим из первой строки записанной матрицы:

$$x_1+x_2+x_3+x_4=1; Rightarrow ; x_1=-x_2-x_3-x_4+1.$$

Случай $kneq<1>$ и $neq<-3>$

Продолжим решение методом Гаусса. Так как $kneq<1>$ и $neq<-3>$, то $(1-k)(k+3)neq<0>$. Следовательно, мы можем разделить вторую и третью строки на $1-k$, четвёртую строку – на выражение $(1-k)(k+3)$. С полученной после этого матрицей продолжим операции обратного хода метода Гаусса:

$$ left(begin 1 & k &1 &1&1\ 0 & 1 &-1 &0&0\ 0 & 0 &1&-1&0\ 0 & 0 &0&1&frac<1>end right) begin r_1-r_4\phantom<0>\phantom<0>\r_3+r_4endrightarrow left(begin 1 & k &1 &0&frac\ 0 & 1 &-1 &0&0\ 0 & 0 &1&0&frac<1>\ 0 & 0 &0&1&frac<1>endright) begin r_1-r_3\r_2+r_3\phantom<0>\phantom<0>endrightarrow\ rightarrowleft(begin 1 & k &0 &0&frac\ 0 & 1 &0 &0&frac<1>\ 0 & 0 &1&0&frac<1>\ 0 & 0 &0&1&frac<1>endright) begin r_1-kcdot\phantom<0>\phantom<0>\phantom<0>endrightarrow left(begin 1 & 0 &0 &0&frac<1>\ 0 & 1 &0 &0&frac<1>\ 0 & 0 &1&0&frac<1>\ 0 & 0 &0&1&frac<1>endright) $$

Из последней матрицы имеем: $x_1=x_2=x_3=x_4=frac<1>$.

  • При $k=-3$ система несовместна.
  • При $k=1$ система является неопределённой. Общее решение системы: $left<begin& x_1=-x_2-x_3-x_4+1;\&x_2in,;x_3in,;x_4in. endright.$
  • При $kneq<-3>$ и $kneq<1>$ система является определённой. Решение системы: $x_1=x_2=x_3=x_4=frac<1>$.

λ-исчисление. Часть первая: история и теория

Идею, короткий план и ссылки на основные источники для этой статьи мне подал хабраюзер z6Dabrata, за что ему огромнейшее спасибо.

UPD: в текст внесены некоторые изменения с целью сделать его более понятным. Смысловая составляющая осталась прежней.

Вступление

Возможно, у этой системы найдутся приложения не только
в роли логического исчисления. (Алонзо Чёрч, 1932)

Вообще говоря, лямбда-исчисление не относится к предметам, которые «должен знать каждый уважающий себя программист». Это такая теоретическая штука, изучение которой необходимо, когда вы собираетесь заняться исследованием систем типов или хотите создать свой функциональный язык программирования. Тем не менее, если у вас есть желание разобраться в том, что лежит в основе Haskell, ML и им подобных, «сдвинуть точку сборки» на написание кода или просто расширить свой кругозор, то прошу под кат.

Начнём мы с традиционного (но краткого) экскурса в историю. В 30-х годах прошлого века перед математиками встала так называемая проблема разрешения (Entscheidungsproblem), сформулированная Давидом Гильбертом. Суть её в том, что вот есть у нас некий формальный язык, на котором можно написать какое-либо утверждение. Существует ли алгоритм, за конечное число шагов определяющий его истинность или ложность? Ответ был найден двумя великими учёными того времени Алонзо Чёрчем и Аланом Тьюрингом. Они показали (первый — с помощью изобретённого им λ-исчисления, а второй — теории машины Тьюринга), что для арифметики такого алгоритма не существует в принципе, т.е. Entscheidungsproblem в общем случае неразрешима.

Так лямбда-исчисление впервые громко заявило о себе, но ещё пару десятков лет продолжало быть достоянием математической логики. Пока в середине 60-х Питер Ландин не отметил, что сложный язык программирования проще изучать, сформулировав его ядро в виде небольшого базового исчисления, выражающего самые существенные механизмы языка и дополненного набором удобных производных форм, поведение которых можно выразить путем перевода на язык базового исчисления. В качестве такой основы Ландин использовал лямбда-исчисление Чёрча. И всё заверте…

λ-исчисление: основные понятия

Синтаксис

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

Мы с вами рассмотрим его наиболее простую форму: чистое нетипизированное лямбда-исчисление, и вот что конкретно будет в нашем распоряжении.

Термы:

переменная: x
лямбда-абстракция (анонимная функция): λx.t , где x — аргумент функции, t — её тело.
применение функции (аппликация): f x , где f — функция, x — подставляемое в неё значение аргумента

Соглашения о приоритете операций:

Может показаться, будто нам нужны какие-то специальные механизмы для функций с несколькими аргументами, но на самом деле это не так. Действительно, в мире чистого лямбда-исчисления возвращаемое функцией значение тоже может быть функцией. Следовательно, мы можем применить первоначальную функцию только к одному её аргументу, «заморозив» прочие. В результате получим новую функцию от «хвоста» аргументов, к которой применим предыдущее рассуждение. Такая операция называется каррированием (в честь того самого Хаскелла Карри). Выглядеть это будет примерно так:

f = λx.λy.t Функция с двумя аргументами x и y и телом t
f v w Подставляем в f значения v и w
(f v) w Эта запись аналогична предыдущей, но скобки явно указывают на последовательность подстановки
((λy.[x → v]t) w) Подставили v вместо x . [x → v]t означает «тело t , в котором все вхождения x заменены на v »
[y → w][x → v]t Подставили w вместо y . Преобразование закончено.

И напоследок несколько слов об области видимости. Переменная x называется связанной, если она находится в теле t λ-абстракции λx.t . Если же x не связана какой-либо вышележащей абстракцией, то её называют свободной. Например, вхождения x в x y и λy.x y свободны, а вхождения x в λx.x и λz.λx.λy.x(y z) связаны. В (λx.x)x первое вхождение x связано, а второе свободно. Если все переменные в терме связаны, то его называют замкнутым, или комбинатором. Мы с вами будем использовать следующий простейший комбинатор (функцию тождества): id = λx.x . Она не выполняет никаких действий, а просто возвращает без изменений свой аргумент.

Процесс вычисления

Рассмотрим следующий терм-применение:

Его левая часть — (λx.t) — это функция с одним аргументом x и телом t . Каждый шаг вычисления будет заключаться в замене всех вхождений переменной x внутри t на y . Терм-применение такого вида носит имя редекса (от reducible expression, redex — «сокращаемое выражение»), а операция переписывания редекса в соответствии с указанным правилом называется бета-редукцией.

Существует несколько стратегий выбора редекса для очередного шага вычисления. Рассматривать их мы будем на примере следующего терма:

который для простоты можно переписать как

(напомним, что id — это функция тождества вида λx.x )

В этом терме содержится три редекса:

  1. Полная β-редукция. В этом случае каждый раз редекс внутри вычисляемого терма выбирается произвольным образом. Т.е. наш пример может быть вычислен от внутреннего редекса к внешнему:
  2. Нормальный порядок вычислений. Первым всегда сокращается самый левый, самый внешний редекс.
  3. Вызов по имени. Порядок вычислений в этой стратегии аналогичен предыдущей, но к нему добавляется запрет на проведение сокращений внутри абстракции. Т.е. в нашем примере мы останавливаемся на предпоследнем шаге:

    Оптимизированная версия такой стратегии (вызов по необходимости) используется Haskell. Это так называемые «ленивые» вычисления.
  4. Вызов по значению. Здесь сокращение начинается с самого левого (внешнего) редекса, у которого в правой части стоит значение — замкнутый терм, который нельзя вычислить далее.

    Для чистого лямбда-исчисления таким термом будет λ-абстракция (функция), а в более богатых исчислениях это могут быть константы, строки, списки и т.п. Данная стратегия используется в большинстве языков программирования, когда сначала вычисляются все аргументы, а затем все вместе подставляются в функцию.

Если в терме больше нет редексов, то говорят, что он вычислен, или находится в нормальной форме. Не каждый терм имеет нормальную форму, например (λx.xx)(λx.xx) на каждом шаге вычисления будет порождать самоё себя (здесь первая скобка — анонимная функция, вторая — подставляемое в неё на место x значение).

Недостатком стратегии вызова по значению является то, что она может зациклиться и не найти существующее нормальное значение терма. Рассмотрим для примера выражение

(λx.λy. x) z ((λx.x x)(λx.x x))

Этот терм имеет нормальную форму z несмотря на то, что его второй аргумент такой формой не обладает. На её-то вычислении и зависнет стратегия вызова по значению, в то время как стратегия вызова по имени начнёт с самого внешнего терма и там определит, что второй аргумент не нужен в принципе. Вывод: если у редекса есть нормальная форма, то «ленивая» стратегия её обязательно найдёт.

Ещё одна тонкость связана с именованием переменных. Например, терм (λx.λy.x)y после подстановки вычислится в λy.y . Т.е. из-за совпадения имён переменных мы получим функцию тождества там, где её изначально не предполагалось. Действительно, назови мы локальную переменную не y , а z — первоначальный терм имел бы вид (λx.λz.x)y и после редукции выглядел бы как λz.y . Для исключения неоднозначностей такого рода надо чётко отслеживать, чтобы все свободные переменные из начального терма после подстановки оставались свободными. С этой целью используют α-конверсию — переименование переменной в абстракции с целью исключения конфликтов имён.

Так же бывает, что у нас есть абстракция λx.t x , причём x свободных вхождений в тело t не имеет. В этом случае данное выражение будет эквивалентно просто t . Такое преобразование называется η-конверсией.

На этом закончим вводную в лямбда-исчисление. В следующей статье мы займёмся тем, ради чего всё и затевалось: программированием на λ-исчислении.

источники:

http://math1.ru/education/sys_lin_eq/kapelli1.html

http://habr.com/ru/post/215807/

Найдите общее решение линейной системы в зависимости от значения параметра . При каких значениях система допускает решение с помощью обратной матрицы?

тогда систему можно записать в виде .

Приравнивая к нулю, найдем, что при и .

Если и , то матрица имеет обратную

и решение имеет вид .

Если аккуратно перемножить и упростить, получим .

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

Можно не использовать обратную матрицу, а применить метод редукции гаусса к расширенной матрице, учитывая, что и ,

При расширенная матрица

Следовательно решения имеют вид , или в матричном виде:

§22.1 $lambda$-матрица

Primary tabs

Forums:

1. $lambda$-матрицей (полиномиальной матрицей) называется матрица, элементы которой являются многочлены относительно некоторой буквы $lambda.$ Степенью $lambda$-матрицы называется наивысшая из степени многочленов, входящих в состав матрицы. Ясно, что $ lambda$- матрица степени $n$ может быть представлена в виде
$$ A_0 lambda^n + A_1 lambda^ + . + A_n, $$
где $ A_k$ — матрицы, уже не зависящие от $ lambda$ *). Частный случай $lambda$ — матриц нам уже встречался неоднократно, а именно матрицы вида $ A — lambda E.$ Результаты, которые мы получим в этом параграфе, для случая $ lambda$-матриц вида $ A — lambda E$ содержат как частный случай многие из результатов, полученных в предыдущих параграфах этой главы.

$lambda$ — матрицы встречаются во всех вопросах математики. Так, например, решение системы однородных линейных дифференциальных уравнений первого порядка с постоянными коэффициентами
$$ <over > = sum_^n a_ y_k (i = 1, 2, . n) qquad qquad (1)$$
ищется обычно в виде
$$ y_k = c_k e^<lambda x>, qquad qquad (2)$$
где $ lambda$ и $c_k$ — некоторые постоянные. Для их определения поставим функции (2) в систему и сократим уравнения на $ e^<lambda x>.$ Мы получим систему линейных уравнений
$$ lambda c_i = sum_^n a_ c_k, $$
матрица которой есть $A — lambda E,$ где $A$ — матрица из коэффициентов системы (1). Таким образом, изучение системы дифференциальных уравнений тесно связано с $ lambda$-матрицей первой степени относительно $ lambda: A — lambda E.$

Аналогично, исследование системы уравнений порядка выше первого приводит к исследованию $ lambda$ — матриц высших степеней. Например, исследование системы уравнений
$$ sum_^n a_ <over > + sum_^n b_ <over > + sum_^n c_ y_k = 0 $$
приводится к исследованию $ lambda$ — матрицы $ A lambda^2 + B lambda C, $ где $ A = ||alpha_|| B = ||b_||, C = ||c_||.$

Мы рассмотрим сейчас вопрос о каноническом виде $ lambda$ — матриц относительно так называемых элементарных преобразований.

Элементарные преобразованиями $ lambda$-матриц называются преобразования следующих типов.

1°. Перестановка между собой двух каких-либо строк или столбцов матрицы.
2°. Прибавление к строке какой-либо другой строки, умноженной на некоторый многочлен $ phi (lambda)$, и, аналогично, прибавление к столбцу другого столбца, умноженного на некоторый многочлен.
3°. Умножение строки или столбца на некоторое число, отличное от нуля.

Определение. Две $ lambda$- матрицы называются эквивалентными, если одна не может быть получена из другой некоторой последовательностью элементарных преобразований.

Обратное к каждому элементарному преобразованию есть снова элементарное преобразование. Это легко проверяется для каждого из трёх типов элементарных преобразований. Так, если $ lambda$-матрица $B(lambda)$ получается из $ lambda$-матрицы $A(lambda)$ перестановкой строк, то обратной перестановкой строк мы можем из $B(lambda)$ получить $A(lambda)$. Если $ B(lambda)$ получается $A(lambda)$ приведением к k-й строке i-й, умноженной на $ phi (lambda),$ то, обратно, $ A(lambda)$ можно получить из $ B(lambda)$ прибавлением к k-й строке i-й, умноженной на — $phi (lambda)$.

Из сделанного замечания следует, что если $ lambda$-матрица $K(lambda)$ эквивалентна $L(lambda),$ то и обратно, $L(lambda)$ эквивалентна $K(lambda).$. В самом деле, пусть из $ K(lambda)$ применением некоторой последовательности элементарных преобразований получается $L(lambda).$ Тогда, применяя к $L(lambda)$ в обратном порядке обратные преобразования, мы придем к $ K(lambda).$

Если две $lambda$-матрицы $ K_1 (lambda)$ и $ K_2 (lambda)$ эквивалентны некоторой матрице $ K(lambda),$ то они эквивалентны между собой. Действительно, если сначала провести последовательность элементарных преобразований, переводящих $ K_1 (lambda)$ в $ K (lambda)$ в $ K_2 (lambda)$, то мы переведем $ K_1(lambda)$ в $K_2(lambda),$ т. е. $K_1 (lambda)$ эквивалентна $ K_2(lambda).$

Основной результат п. 1 этого параграфа состоит в доказательстве теоремы о то, что всякую $ lambda$ — матрицу можно элементарными преобразованиями привести к диагональному виду. Доказательству этого предположения предпошлем лемму:

Лемма. Если элемент $a_ <11>(lambda)$ в $lambda$ — матрице $ A(lambda)$ не равен нулю и если не все элементы $a_ (lambda)$ матрицы $ A(lambda)$. делятся на многочлен $a_ <11>(lambda),$ то можно подобрать эквивалентную $ A(lambda) lambda$- матрицу $B(lambda),$ для которой элемент $b_ <11>(lambda)$ также не равен нулю и имеет степень более низкую, чем $ a_ <11>(lambda).$

Доказательство. Предположим сначала, что не делящийся на $a_<11>(lambda)$ элемент матрицы $A (lambda)$ находится в первой строке. Пусть, например, $a_ (lambda)$ не делится на $a_ <11>(lambda).$ Тогда $ a_ <1k>(lambda)$ можно представить в виде
$$ a_ <1k>(lambda) = a_ <11>(lambda) phi(lambda) + b(lambda),$$
где $ phi (lambda) $ — частное, $ b(lambda) ≠ 0$ — остаток от деления $ a_ <1k>(lambda)$ на $a_ <11>(lambda)$ и, следовательно, степень $b(lambda)$ ниже, чем степень $ a_ <11>(lambda).$ Вычтем из k-го столбца первый, умноженный на $ phi (lambda).$ Получим матрицу, где вместо $a_ <1k>(lambda)$ стоит теперь многочлен $b(lambda),$ имеющий более низкую степень, чем $ a_ <11>(lambda).$ Переставляя теперь k-й столбец с первым, мы переведем $ b(lambda)$ в левый верхний угол.

Рассмотрим теперь случай, когда все элементы первой строки и первого столбца делятся на $a_ <11>(lambda),$ а некоторый элемент $a_ (lambda)$ не делится на $ a_ <11>(lambda).$ Это случай мы сведём к предыдущему следующим образом: $ a_ (lambda)$ делится на $a_ <11>(lambda),$ т. е. имеет вид $ a_ (lambda) = phi (lambda) a_ <11>(lambda).$ Вычтем из i-й строки первую, умноженную на $ phi (lambda).$ Тогда $ a_ (lambda)$ заменится нулем, элемент $ a_ (lambda)$ заменится элементом $ a_ (lambda) = a_ (lambda) — phi (lambda) a_ <1k>(lambda),$ который по-прежнему не делится на $ a_ <11>(lambda) $. (так как $ a_ <1k>(lambda)$ по предположению делится на на $ a_ <11>(lambda)).$ Прибавим теперь i-ю строку к первой. Так как на первом месте в i-й строке теперь стоит нуль, то $ a_ <11>(lambda)$ не изменится, а на k-м месте в первой строке теперь будет стоять $ a_ <1k>(lambda) + a_ (lambda) = a_ <1k>(lambda) (1 — phi (lambda)) + a_ (lambda)$ и, следовательно, в первой строке имеется элемент, не делящийся на d$ a_ <11k>(lambda).$ Мы свели этот случай к рассмотренному выше и, следовательно, лемма доказана.

В дальнейшем мы будем пользоваться также следующим замечанием: если все элементы $ lambda$-матрицы $B (lambda)$. делятся на некоторый многочлен $E(lambda),$ то после элементарных преобразований над матрицей $ B(lambda)$ мы снова получим матрицу, элементы которой делятся на $ E(lambda)$.

Перейдем теперь к проведению $lambda$-матрицы к диагональному виду.

Мы можем считать, что $ a_ <11>(lambda) ≠ 0,$ так как, если в матрице есть хоть один элемент, отличный от нуля, то перестановками строк и столбцов его можно перевести на это место. Если не все элементы матрицы делятся на $a_ <11>(lambda),$ то мы можем способом, указанным в лемме, заменить матрица эквивалентной, в которой элемент, стоящий в левом верхнем углу, имеет более низкую степень и по-прежнему отличен от нуля. Если не все элементы делятся на него, то мы можем опять понизить степень этого элемента и т. д. Процесс закончится, когда мы придем к матрице $B(lambda)$, в которой все элементы делятся на $ b_ <11>(lambda).$

Так как элементы $b_ <12>(lambda), . b_ <1n>(lambda)$ первой строки делятся на $ b_ <11>(lambda),$ то вычитая из второго, третьего и т. д. столбца первый, умноженый на соответственно подобранные многочлены от $ lambda,$ мы можем обратить в нуль 2-й, 3-й, . n-й элементы первой строки. Аналогично обратим в нуль все элементы, начиная со второго, в первом столбце. Так как в матрице $B(lambda)$ все элементы делились на $b_ <11>(lambda),$ то в полученное матрице все элементы также делятся на $b_ <11>(lambda).$ Разделим все элементы первой строки на старший коэффициент многочлена $b_ <11>(lambda).$ На первом месте получится многочлен со старшим коэффициентом 1, который мы обозначим через $E_1 (lambda),$ а на остальных местах будут по-прежнему нули.

Мы пришли, таким образом, к матрице следующего вида:
$$ beginE_1 (lambda) & 0 & 0 . 0 \
0 & c_ <22>(lambda) & c_ <23>(lambda) . c_ <2n>(lambda) \
cdots & cdots & cdots \
0 & c_ (lambda) & c_ (lambda) . c_ (lambda)
end, qquad (3) $$
все элементы которой делятся на $E_1 (lambda).$

Мы можем теперь повторить с матрицей $(n-1)$-го порядка $ ||c_ (lambda)||$ те же операции, что с матрицей n-го порядка. Заметим, что всякое элементарное преобразование матрицы $||c_||$ есть в то же время элементарное преобразование матрицы (3), так как в первой строке и столбце все элементы кроме $E_1(lambda)$ равны нулю.

Таким образом, мы обратим в нуль все элементы второй строки и второго столбца, кроме диагонального. Полученный диагональный элемент (старший коэффициент которого также считаем равным единице) обозначим $E_2 (lambda).$ Все элементы $c_ (lambda)$ делятся на $E_1 (lambda).$ Поэтому все дальнейшие элементарные преобразования всегда приводят нас к элементам, делящийся на $E_1 (lambda).$ В частности, $ E_2(lambda)$ делятся на $E_1 (lambda).$

Мы пришли, таким образом, к матрице, у которой в первых двух строках и столбцах все элементы кроме диагональных равны нулю, а по диагонали стоят $E_1 (lambda)$ и $E_2 (lambda),$ причем $E_2 (lambda)$ делится на $E_1 (lambda).$ Мы сможем продолжать этот процесс далее, пока не приведем всю матрицу к диагональному виду. Может, конечно, оказаться, что мы закончим процесс раньше, придя к матрице, состоящей сплошь из нулей.
Итак, доказана следующая

Теорема 1. Всякая $lambda$ — матрица может быть элементарными преобразованиями приведена к виду

$$ beginE_1 (lambda) & 0 & 0 . 0 \
0 & E_2 (lambda) & 0 . 0 \
0 & 0 & E_3(lambda) . 0 \
cdots $ cdots & cdots \
0 & 0 & 0 . E_n(lambda)
end, qquad (4)$$
где многочлены $ E_k (lambda),$ стоящие по диагонали, имеют старшие коэффициенты, равные единице, многочлен $E_2 (lambda)$ делится на $E_1 (lambda), E_3 (lambda)$ делится на $ E_2 (lambda), E_4(lambda)$ на $E_3 (lambda)$ и т. д. Этот вид называется нормальной диагональной формой $ lambda$ — матрицы.

Конечно, некоторое число последних многочленов $ E_k (lambda)$ в матрице (4) может оказаться равным нулю:
$$ E_ (lambda) = E_ (lambda) = . = 0$$

Замечание. Мы привели матрицу $A (lambda)$ к нормальному диагональному виду, в котором каждый диагональный элемент делится на предшествующий. Если поставить себе целью приведение матрицы
к какому-нибудь диагональному виду, отбросив требование делимости, то задача решается проще.

Действительно, для того чтобы обратить в нуль все элементы первой строки и первого столбца кроме $a_ <11>(lambda),$ достаточно, чтобы эти элементы (а не все элементы матрицы) делились на $a_ <11>(lambda).$ Как видно из доказательства леммы, для того чтобы этого достигнуть, требует гораздо меньше число элементарных преобразований, чем для приведения к нормальной диагональной форме. Обратив в нуль все элементы первой строки и первого столбца кроме диагонального, мы можем проделать то же самое с оставшейся матрицей (n-1)-го порядка и т. д., пока матрица не будет приведена к диагональному виду. Этим путем можно привести матрицу к различным диагональным формам, т. е. диагональная форма не определена однозначно. В следующем пункте этого параграфа мы покажем, что нормальная диагональная форма данной $lambda$ — матрицы определяется уже однозначно.

Управление. Перевести $lambda$-матрицу
$$ beginlambda — lambda_1 & 0 \
0 & lambda — lambda_2
end, lambda_1 ≠ lambda_2, $$
к нормальной диагональной форме.
Ответ
$$ begin1 & 0 \
0 (lambda — lambda_1) (lambda — lambda_2).
end.$$

2. В этом пункте мы докажем, что нормальная диагональная форма данной матрицы определена однозначно. Для этого мы построим систему многочленов, связанных с данной $ lambda$-матрицей, которые не меняются при элементарных преобразованиях и которыми, как мы увидим, нормальная диагональная форма $ lambda$-матрицы вполне определяется.

Пусть дана произвольная $ lambda$-матрица. Наибольший общий делитель всех миноров k-го порядка данной $ lambda$ — матрицы обозначим через $D_k (lambda).$ Так как наибольший общий делитель определен с точностью до постоянного множителя, то будем считать, ,то старший коэффициент у $D_k (lambda)$ равен единице. В частности, если общий наибольший делитель миноров k-го порядка равен постоянной, то мы полагаем $ D_k (lambda) =1. $

Докажем, что элементарные преобразования не меняют многочленов $D_k (lambda),$ т. е. что у эквивалентных $ lambda$-матриц многочлены $ D_k (lambda)$ совпадают.

Для элементарных преобразований вида 1°, переставляющих строки или столбцы, это очевидно, так как при них каждый минор k-го порядка либо вовсе не меняется, либо меняет знак, либо заменяется другим минором k-го порядка, что, конечно, не меняет общего наибольшего делителя всех таких миноров. Аналогично, не меняют $ D_k (lambda)$ элементарные преобразования вида 3°, так как при этих преобразованиях миноры самое большее умножаются на постоянное. Рассмотрим теперь элементарное преобразование вида 2°, например, прибавим к i-мц столбцу j-й, умноженный на $phi (lambda).$ При этом минор k-го порядка вовсе не изменится, если он содержит и i-й и j-й столбцы, либо если он не содержит ни одного из них.

В случае же, если минор содержит i-й столбец и не содержит j-го столбца, то его можно представить как комбинацию двух миноров, которые имелись у исходной матрицы. Таким образом, наибольший общий делитель миноров k-го порядка и в этом случае не изменится.

Если все миноры порядка $k,$ а следовательно, и более высоких порядков, матрицы $A(lambda)$ равны нулю, то мы будем считать $D_k +(lambda) = D_ (lambda) = . = D_n (lambda) = 0.$ Заметим, что из совпадения у всех эквивалентных матриц многочленов $ D_k (lambda)$ следует, что эквивалентные матрицы имеют один и тот же ранг.

Найдем многочлены $D_k (lambda)$ для матрицы, приведенной к нормальной диагональной форме:

$$ beginE_1 (lambda) & 0 & . 0 \
0 & E_2 (lambda) . 0 \
cdots & cdots & cdots \
0 & 0 . E_n (lambda)
end. qquad qquad (5)$$

Заметим, что у диагональной матрицы отличны от нуля только главные миноры, т. е. миноры, в которые входят строки и столбцы с одинаковыми номерами. Эти миноры имеют вид $ E_i, (lambda) E_ (lambda) . E_ (lambda).$

Так как $ E_2 (lambda)$ делится на $ E_1 (lambda), E_3 (lambda)$ делится на $E_2(lambda)$ и т. д.. , то наибольший общий делитель миноров первого порядка $D_1 (lambda)$ равен $E_1 (lambda).$ Так как все многочлены $E_k (lambda)$ делятся на $ E_1 (lambda),$ а все многочлены кроме $ E_1 (lambda)$ делятся на $ E_2 (lambda)$, то произведение $ E_i (lambda) E_j (lambda) ( i

Таким же образом для матрицы (4)
$$ D_k (lambda) E_1 (lambda) E_2 (lambda) . E_k (lambda) (k = 1, 2, . n). qquad (6)$$

Очевидно, что если, начиная с некоторого $ r, E_ (lambda) = E_ (lambda) = . = E_n (lambda) = 0,$ то $ D_ (lambda) = D_ (lambda) = . = D_n (lambda) = 0.$
Отсюда получается, что для $lambda$-матрицы, имеющей нормальную диагональную форму (5), диагональны элементы $ E_k (lambda)$ вычисляются по формулам
$$ E_k (lambda) = <over (lambda)>>. $$

При этом, если $ D_ (lambda) = . = D_n (lambda) = 0,$ то надо положить $ E_ (lambda) = . = E_n (lambda) = 0.$

Многочлены $E_k (lambda)$ называются инвариантным множителями. В параграфе 20 мы уже определили их для матриц вида $A — lambda E.$

Теорема 2. Нормальная форма данной $lambda$-матррцы $A (lambda)$ определяется по ней однозначно. Если $ D_k (lambda) (k = 2, 3, . r)$-наибольший общий делитель миноров k-го порядка матрицы $ A (lambda), $ а $D_ (lambda) = . = D_n (lambda) = 0,$ то элементы нормальной диагональной формы определяются по формулам
$$ E_k (lambda) = <over (lambda)>> (k = 1, 2, . r), $$
а
$$ E_ (lambda) = E_ (lambda) (lambda) = . = E_n (lambda) = 0.$$

Доказательство. Мы показали, что при элементарных преобразованиях многочлены $ D_k (lambda)$ не меняются. Поэтому, если матрица $A(lambda)$ эквивалентна диагональной нормальной матрице (5), то $D_k (lambda)$ у них совпадают. Так как для матрицы (5) мы получили, что
$$ D_k (lambda) = E_1 (lambda) . E_k (lambda) (k = 1, 2, . r; r leqslant n)$$
и что $ D_ (lambda) = D_ (lambda) = . = D_n (lambda) = 0,$ то теорема доказана.

Следствие. Для того чтобы две $lambda$-матрицы $ A(lambda)$ и $ B(lambda)$ были эквивалентны, необходимо и достаточно, чтобы для них совпадали многочлены $ D_1 (lambda), D_2 (lambda), . D_n (lambda).$

Действительно, если многочлены $ D_k (lambda)$ у $A(lambda)$ и $ B(lambda)$ совпадают, то эти матрицы эквивалентны одной и той же нормальной диагональной $ lambda$-матрице и, следовательно, эквивалентны между собой.

3. Назовем $lambda$-матрицу $P(lambda)$ обратимой, если матрица $ [P(lambda)^<-1>$ также есть $lambda$-матрица. Если $ Det P(lambda)$ равен постоянной, отличной от нуля, то $P(lambda)$ обратима. Действительно, элементы обратной матрицы равны минорам $(n-1)$-го порядка, деленным на $ Det P(lambda),$ т. е. в нашем случае они будут многочленами от $lambda$ и, значит, $ [P (lambda)]^ <-1>$ будет $ lambda$-матррцей. Обратно, если $ P(lambda)$ обратима, то $ Det P(lambda) = const ≠ 0.$ В самом деле, пусть $ [P(lambda)]^ <-1>= P_1 (lambda).$ Тогда $ Det P (lambda) Det P_1 (lambda) = 1,$ а произведение двух многочленов может быть тождественно равно единице лишь в том случае, если многочлены суть отличные от нуля постоянные. Таким образом, мы показали, что $lambda$-матрица обратима тогда и только тогда, когда ее определитель есть постоянная, отличная от нуля.

Все обратимые матрицы эквивалентны единичной матрице. В самом деле, определитель обратимой матрицы равен постоянной, отличной от нуля, и, значит, $D_n (lambda) = 1.$ Так как $ D_n (lambda)$ делится на $ D_k (lambda)$, то и $ D_k (lambda) = 1 (k = 1, 2, . n).$ Поэтому все инвариантные множители $ E_k (lambda)$ обратимой матрицы равны 1, и нормальная диагональная форма для них будет совпадать с единичной матрицей.

Теорема 3. Для того чтобы $lambda$-матрицы $A (lambda)$ и $B (lambda)$ были эквивалентны между собой, необходимо и достаточно, чтобы существовали обратимые $lambda$-матрицы $ P(lambda)$ и $ Q(lambda)$ такие, что
$$ A(lambda) = P (lambda) B (lambda) Q (lambda). qquad qquad (7)$$

Доказательство. Докажем сначала, что если матрицы $ A (lambda)$ и $ B(lambda)$ эквивалентны, то можно подобрать обратимые матрицы $ P(lambda)$ и $ Q(lambda)$ так, чтобы выполнялось равенство (6). Для этого заметим, что каждое элементарное преобразование $ lambda$-матрицы $ A (lambda)$ можно осуществить, умножая $ A(lambda)$ слева или справа на некоторую обратимую $ lambda$- матрицу — матрицу этого элементарного преобразования.

Покажем, что это для всех трёх типов элементарных преобразований. Пусть дана $ lambda$-матрица
$$ A(lambda) = begina_ <11>(lambda) a_ <12>(lambda) . a_ <1n>(lambda) \
a_ <21>(lambda) a_ <22>(lambda) . a_ <2n>(lambda) \
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \
a_ (lambda) a_ (lambda) . a_ (lambda)
end. $$
Чтобы поменять местами, например, первый и второй столбцы (соответственно строки) этой матрицы, надо умножить $ A(lambda)$ справа (соответственно слева) на матрицу
$$ begin
0 $ 1 & 0 . 0 \
1 & 0 & 0 . 0 \
0 & 0 & 1 . 0 \
cdots & cdots & cdots \
0 & 0 & 0 . 1
end, qquad qquad (8)$$
полученную из единичной перестановкой тех же столбцов (или, что все равно, строк).

Чтобы умножить второй столбец матрицы $ A (lambda)$ на число $ alpha$, нужно умножить $ A (lambda)$ справа (соответственно слева) на матрицу
$$ begin
1 & 0 & 0 . 0 \
0 & alpha & 0 . 0 \
0 & 0 & 1 . 0 \
cdots & cdots & cdots
0 & 0 & 0 . 1
end, qquad (9)$$
полученную из единичной также умножением на $ alpha$ второго столбца (строки).

Наконец, чтобы прибавить к первому столбцу $A (lambda)$ второй, умноженный на $ phi (lambda)$, надо умножить $ A (lambda)$ справа на матрицу
$$ begin1 & 0 & 0 . 0 \
phi (lambda) & 1 & 0 . 0 \
0 & 0 & 1 . 0 \
cdots & cdots & cdots \
0 & 0 & 0 & 1
end, qquad qquad (10)$$
полученную с помощью той же операции из единичной, а чтобы прибавить к первой строке вторую, умноженную на $ phi (lambda),$ нужно умножить $ A (lambda)$ слева на матрицу
$$ begin
1 & phi (lambda) & 0 . 0 \
0 & 1 & 0 . 0 \
0 & 0 & 1 . 0 \
cdots & cdots cdots \
0 & 0 & 0 . 1
end, qquad qquad (11)$$
которая также получается из единичной с помощью соответствующего элементарного преобразования.

Мы видим, таким образом, что матрицы элементарных преобразований — это матрицы, полученные одним элементарным преобразованием из $ E,$ причем, чтобы произвести элементарное преобразование над столбцами, $ A(lambda)$ надо умножать на матрицу преобразования справа, а чтобы преобразовать строки, $ A (lambda)$ умножать на матрицу слева.

Можно сосчитать определитель каждой из приведенных матриц и, таким образом, проверить, что он равен отличной от нуля постоянной; следовательно, все эти матрицы обратимы. Так как определитель произведения матриц равен произведению определителей, то и произведение матриц элементарных преобразований есть обратимая матрица.

Так как мы предположили, что $ A (lambda)$ и $ B(lambda)$ эквивалентны, то $ A (lambda)$ можно получить, применяя к $ B(lambda)$ некоторую цепочку преобразований. Каждое элементарное преобразование можно осуществить, умножая $ B(lambda)$ на обратимую $ lambda$-матрицу; следовательно, весь переход от $ B(lambda)$ к $ A (lambda)$ можно получить, умножая $ B(lambda)$ последовательно на некоторую совокупность обратимых $ lambda$-матриц слева и справа. Так как произведение обратимых матриц также есть обратимая матрица, то первая часть теоремы тем самым доказана.

Отсюда следует, что всякая обратимая матрица есть произведение матриц элементарных преобразований. Действительно, всякая обратимая матрица $ Q (lambda)$ эквивалентна единичной матрице и поэтому может быть представлена в виде
$$ Q (lambda) = P_1 (lambda) EP_2 (lambda),$$
где $ P_1 (lambda) $ и $ P_2 (lambda)$ — произведения элементарных преобразований. Но это значит, что и сама $ Q (lambda) = P_1 (lambda) P_2 (lambda)$ есть произведение матриц элементарных преобразований.

Этим замечанием можно воспользоваться для доказательства второй половины теоремы. Действительно, пусть дано, что
$$ A(lambda) = P (lambda) B(lambda) Q (lambda),$$
где $ P(lambda)$ и $Q (lambda)$ обратимы. Но, согласно только что сделанному замечанию, умножение слева на $ P(lambda)$ и справа на $ Q (lambda)$ эквивалентно некоторой совокупности элементарных преобразований, произведенных над $ B (lambda).$ Таким образом, $ A (lambda)$ эквивалентна $ B(lambda),$ что и требовалось доказать.

4. В этом пункте мы будем заниматься $ lambda$-матрицами вида $ A — lambda E,$ где $ A$-постоянная матрица. Основной вопрос, который будет решен, это вопрос об эквивалентности $ lambda$-матриц первой степени $ A — lambda E$ и $ B — lambda E).$

Легко видеть, что если матрицы $ A$ и $ B$ подобны, т. е. существует такая невырожденная постоянная матрица $ C,$ что $ B = C^ <-1>AC,$ то $ lambda$-матрицы $ A — lambda E$ и $ B — lambda E$ эквивалентны. Действительно, если
$$ B = C^ <-1>AC,$$
то
$$ B — lambda E = C^ <-1>(A — lambda E) C.$$

Так как постоянная невырожденная матрица есть частный случай обратимой $ lambda$-матрицы, то, по теореме 3, этого равенства следует эквивалентность $ A — lambda E$ и $ B — lambda E.$

Мы покажем позднее и обратное, что из эквивалентности $ lambda$-матриц $ A — lambda E$ и $ B — lambda E$ следует подобие матриц $ A$ и $ B.$ Отсюда мы получим, в частности, новое доказательство того, что всякая матрица подобна матрице, имеющей нормальную жорданову форму.

Доказательству предпошлем лемму:
Лемма. Произвольную $ lambda$-матрицу
$$ P(lambda) = P_0 lambda^n + P_1 lambda^ + . + P_n $$
можно разделить слева на матрицу вида $ A — lambda E$ (где $A$-любая постоянная матрица), т. е. можно найти такие матрицы $ S (lambda)$ и $ R (R$ постоянна), что,
$$ P (lambda) = (A — lambda E) S (lambda) + R. $$

Процесс деления, с помощью которого доказывается лемма, отличается от обычного деления многочленов только тем, что при умножении нельзя изменять порядок сомножителей.
Пусть
$$ P (lambda) = P_0 lambda^n + P_1 lambda^ + . + P_n, $$
где $ P_k$ — постоянные матрицы.
Легко видеть, что $ lambda$-матрица
$$ P (lambda) + (A — lambda E) P_0 lambda^ $$
будет иметь степень выше $ n-1$.

Если
$$ P(lambda) + (A — lambda E) P_0 lambda^ = P_0′ lambda^ + . + P_’, $$
то аналогично многочлен
$$ P(lambda) + (A — lambda E) P_0 lambda^ + (A — lambda E) P_0′ lambda^$$
есть многочлен степени не выше $n-2.$ Продолжая этот процесс, мы придем к многочлену
$$ P(lambda) + (A — lambda E) ( P_0 lambda^ + P_0′ lambda^ + P_0′ lambda^ + . ) $$
степени не выше нулевой, т. е. не зависящую от $ lambda.$ Обозначив полученную постоянную матрицу через $ R,$ мы получим
$$ P(lambda) = (A — lambda E) [- P_0 lambda^ — P_0′ lambda^ + . ] + R.$$
Если теперь обозначить многочлен в квадратных скобках через $ S (lambda)$, то мы будем иметь
$$ P(lambda) = (A — lambda E) S (lambda) + R,$$
т. е. лемма доказана.

Аналогично доказывается возможность деления справа, т. е. существование матриц $ S_1 (lambda)$ и $ R_1$ таких, что
$$ P(lambda) = S_1 (lambda) (A — lambda E) + R_1.$$
Заметим кстати, что здесь, как и в обычной теореме Безу, можно утверждать, что
$$ R = R_1 = P(A).$$

Теорема 4. Для того чтобы $ lambda$-матрицы $ A — lambda E$ и $ B — lambda E$ были эквивалентны, необходимо и достаточно, чтобы матрицы $A$ и $ B$ были подобны.

Доказательство. Достаточность была доказана в начале этого пункта. Докажем необходимость. Нам надо доказать, что если $ lambda$-матрицы $ A — lambda E$ и $ B — lambda E$ эквивалентны, то матрицы $ A $ и $ B$ подобны. Существует такие обратимые $ lambda$-матрицы $ P(lambda)$ и $ Q(lambda)$, что
$$ B — lambda E = P(lambda) (A — lambda E) Q (lambda). qquad qquad (12)$$

Покажем сначала, что в равенстве (12) $ P(lambda) $ и $ Q (lambda)$ можно заменить постоянными матрицами.

С этой целью разделим $ P(lambda)$ на $B — lambda E$ слева, $ Q (lambda)$-справа. Мы получим равенства
$$ P (lambda) = (B — lambda E) P_1 (lambda) + P_0, \
Q (lambda) = Q_1 (lambda) (B — lambda E) + Q_0, qquad qquad (13)$$
где $ P_0$ и $ Q_0$ — постоянные матрицы.

Подставив в формулу (12) выражение для $ P (lambda)$ и произведем умножение. Мы получим:
$$ B — lambda E = (B — lambda E) P_1 (lambda) (A — lambda E) Q (lambda) + P_0 (A — lambda E) Q (lambda).$$
Во второе слагаемое подставим выражение для $ Q(lambda),$ произведем умножение и перенесем слагаемое $ P_0 (A — lambda E) Q_0$ в левую часть равенства. Мы получим:
$$ B — lambda E — P_0 (A — lambda E) Q_0 = K (lambda), qquad (14)$$

где
$$ K (lambda) = (B — lambda E) P_1 (lambda) (A — lambda E) Q (lambda) + \
+ P_0 (A — lambda E) Q_1 (lambda) (B — lambda E). qquad (15)$$

Из равенства (13) следует, что $P_0 = P(lambda) — (B — lambda E) P_1 (lambda).$ Заменив этим выражением $ P_0$ во втором слагаемом, получим
$$ K (lambda) = (B — lambda E) P_1 (lambda) (A — lambda E) Q (lambda) + \
+ P(lambda) (A — lambda E) Q_1 (lambda) (B — lambda E) — \
— (B — lambda E) P_1 (lambda) (A — lambda E) Q_1 (lambda) (B — lambda E). qquad (16)$$
Но из равенства (12) мы имеем
$$ (A — lambda E) Q (lambda) = P^ <-1>(lbda) (B — lambda E), \
P(lambda) (A — lambda E) = (B — lambda E) Q^ <-1>(lambda).$$
Пользуясь этими равенства и, мы можем ввести множитель $ B — lbda E$ в конец первого и начало второго слагаемого в выражении для $ K (lbda),$ после чего получим окончательно
$$ K (lambda) = (B — lambda E) [P_1 (lambda) P^ <-1>(lambda) + Q^ <-1>(lambda) Q_1 (lambda)- \
— P_1 (lambda) (A — lambda E) Q_1 (lambda)] (B — lambda E).$$
Докажем теперь, что $ K (lambda) = 0.$ Выражение в квадратных скобках, в силу обратимости $ P(lambda)$ и $ Q(lambda)$, есть многочлен относительно $ lambda.$ Докажем, что он равен нулю. Предположим, что этот многочлен отличен от нуля и имеет степень $m.$ Нетрудно убедиться тогда, что $ K (lambda)$ имеет степень $ m+2$ и так как $ m >geqslant 0,$ является многочленом не ниже второй степени. Далее следует, что $ K(lambda)$ не выше первой степени. Следовательно, выражение в квадратных скобках, а значит, и $ K (lambda) = 0.$
Мы получили таким образом, что
$$ B — lambda E = P_0 (A — lambda E) Q_0, qquad qquad (17)$$
где $ P_0$ и $ Q_0$-постоянные матрицы, т. е. в равенстве (12) можно матрицы $ P(lambda), Q(lambda)$ заменить постоянными матрицами.

Сравнивая коэффициенты при первой степени $ lambda$ в обеих частях равенства (17), мы получаем
$$ P_0 Q_0 = E,$$
откуда следует невырожденность каждой из матриц $ P_0$ и $ Q_0$ и равенство
$$ P_0 = Q_0^<-1>.$$

Сравнение свободных членов даёт
$$ B = P_0 AQ_0 = Q_0^ <-1>AQ_0,$$
т. е. $B$ и $A$ подобны. Теорема доказана.

Так как условием эквивалентности $ A -lambda E$ и $ B — lambda E$ служит совпадение их инвариантных множителей, то из доказанной теоремы следует, что, для того чтобы матрицы $A$ и $B$ были подобны, необходимо и достаточно, чтобы инвариантные множители у $ A-lambda E$ и $ B — lambda E$ совпадали между собой. Покажем теперь, что всякая матрица $ A$ подобна матрицей, имеющей жорданову нормальную форму.

Для этого рассмотрим матрицу $ A — lambda E$ и найдем ее инвариантные множители. По этим инвариантным множителям построим матрицу $ B$, имеющую жорданову нормальную форму. Тогда $ B — lambda E$ имеет те же инвариантные множители, что и $ A — lambda E,$ и, значит, $ B$ подобно $A.$

источники:

http://forany.xyz/t-175

http://fkn.ktu10.com/?q=node/11589

Как найти лямбду

Буквой λ (лямбда) обозначается длина волны того или иного излучения. Эту величину можно измерить, можно рассчитать теоретически, а если излучение является видимым, то даже определить на глаз.

Как найти лямбду

Инструкция

Чтобы рассчитать длину волны излучения, зная частоту и скорость распространения этого излучения, поделите вторую величину на первую. Если же вместо частоты известен период, умножьте его на скорость распространения излучения. Наконец, если известна циклическая частота излучения, умножьте скорость на 2π, а затем результат поделите на циклическую частоту.
Чтобы результат получился в системе СИ, предварительно переведите в нее же все величины из условия задачи. Затем переведите результат обратно в удобные для вас единицы.

Если излучение является световым, длину его волны в вакууме определите на глаз: красный — от 635 до 690 нм, оранжевый — 590, желтый — от 570 до 580, зеленый — от 510 до 520, синий — от 440 до 480, фиолетовый — от 380 до 400.

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

Для нахождения длины волны излучения дециметрового или сантиметрового диапазона подключите антенну к волномеру, после чего начните плавно менять ее размер. Когда он станет равен половине длины волны, показания волномера окажутся максимальными.

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

Войти на сайт

или

Забыли пароль?
Еще не зарегистрированы?

This site is protected by reCAPTCHA and the Google Privacy Policy and Terms of Service apply.

λ-исчисление. Часть первая: история и теория

Время на прочтение
6 мин

Количество просмотров 146K

Идею, короткий план и ссылки на основные источники для этой статьи мне подал хабраюзер z6Dabrata, за что ему огромнейшее спасибо.

UPD: в текст внесены некоторые изменения с целью сделать его более понятным. Смысловая составляющая осталась прежней.

Вступление

Возможно, у этой системы найдутся приложения не только
в роли логического исчисления. (Алонзо Чёрч, 1932)

Вообще говоря, лямбда-исчисление не относится к предметам, которые «должен знать каждый уважающий себя программист». Это такая теоретическая штука, изучение которой необходимо, когда вы собираетесь заняться исследованием систем типов или хотите создать свой функциональный язык программирования. Тем не менее, если у вас есть желание разобраться в том, что лежит в основе Haskell, ML и им подобных, «сдвинуть точку сборки» на написание кода или просто расширить свой кругозор, то прошу под кат.

Начнём мы с традиционного (но краткого) экскурса в историю. В 30-х годах прошлого века перед математиками встала так называемая проблема разрешения (Entscheidungsproblem), сформулированная Давидом Гильбертом. Суть её в том, что вот есть у нас некий формальный язык, на котором можно написать какое-либо утверждение. Существует ли алгоритм, за конечное число шагов определяющий его истинность или ложность? Ответ был найден двумя великими учёными того времени Алонзо Чёрчем и Аланом Тьюрингом. Они показали (первый — с помощью изобретённого им λ-исчисления, а второй — теории машины Тьюринга), что для арифметики такого алгоритма не существует в принципе, т.е. Entscheidungsproblem в общем случае неразрешима.

Так лямбда-исчисление впервые громко заявило о себе, но ещё пару десятков лет продолжало быть достоянием математической логики. Пока в середине 60-х Питер Ландин не отметил, что сложный язык программирования проще изучать, сформулировав его ядро в виде небольшого базового исчисления, выражающего самые существенные механизмы языка и дополненного набором удобных производных форм, поведение которых можно выразить путем перевода на язык базового исчисления. В качестве такой основы Ландин использовал лямбда-исчисление Чёрча. И всё заверте…

λ-исчисление: основные понятия

Синтаксис

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

только хардкор

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

Мы с вами рассмотрим его наиболее простую форму: чистое нетипизированное лямбда-исчисление, и вот что конкретно будет в нашем распоряжении.

Термы:

переменная: x
лямбда-абстракция (анонимная функция): λx.t, где x — аргумент функции, t — её тело.
применение функции (аппликация): f x, где f — функция, x — подставляемое в неё значение аргумента

Соглашения о приоритете операций:

Может показаться, будто нам нужны какие-то специальные механизмы для функций с несколькими аргументами, но на самом деле это не так. Действительно, в мире чистого лямбда-исчисления возвращаемое функцией значение тоже может быть функцией. Следовательно, мы можем применить первоначальную функцию только к одному её аргументу, «заморозив» прочие. В результате получим новую функцию от «хвоста» аргументов, к которой применим предыдущее рассуждение. Такая операция называется каррированием (в честь того самого Хаскелла Карри). Выглядеть это будет примерно так:

f = λx.λy.t Функция с двумя аргументами x и y и телом t
f v w Подставляем в f значения v и w
(f v) w Эта запись аналогична предыдущей, но скобки явно указывают на последовательность подстановки
((λy.[x → v]t) w) Подставили v вместо x. [x → v]t означает «тело t, в котором все вхождения x заменены на v»
[y → w][x → v]t Подставили w вместо y. Преобразование закончено.

И напоследок несколько слов об области видимости. Переменная x называется связанной, если она находится в теле t λ-абстракции λx.t. Если же x не связана какой-либо вышележащей абстракцией, то её называют свободной. Например, вхождения x в x y и λy.x y свободны, а вхождения x в λx.x и λz.λx.λy.x(y z) связаны. В (λx.x)x первое вхождение x связано, а второе свободно. Если все переменные в терме связаны, то его называют замкнутым, или комбинатором. Мы с вами будем использовать следующий простейший комбинатор (функцию тождества): id = λx.x. Она не выполняет никаких действий, а просто возвращает без изменений свой аргумент.

Процесс вычисления

Рассмотрим следующий терм-применение:

(λx.t) y

Его левая часть — (λx.t) — это функция с одним аргументом x и телом t. Каждый шаг вычисления будет заключаться в замене всех вхождений переменной x внутри t на y. Терм-применение такого вида носит имя редекса (от reducible expression, redex — «сокращаемое выражение»), а операция переписывания редекса в соответствии с указанным правилом называется бета-редукцией.

Существует несколько стратегий выбора редекса для очередного шага вычисления. Рассматривать их мы будем на примере следующего терма:

(λx.x) ((λx.x) (λz. (λx.x) z)),

который для простоты можно переписать как

id (id (λz. id z))

(напомним, что id — это функция тождества вида λx.x)

В этом терме содержится три редекса:

  1. Полная β-редукция. В этом случае каждый раз редекс внутри вычисляемого терма выбирается произвольным образом. Т.е. наш пример может быть вычислен от внутреннего редекса к внешнему:
  2. Нормальный порядок вычислений. Первым всегда сокращается самый левый, самый внешний редекс.
  3. Вызов по имени. Порядок вычислений в этой стратегии аналогичен предыдущей, но к нему добавляется запрет на проведение сокращений внутри абстракции. Т.е. в нашем примере мы останавливаемся на предпоследнем шаге:

    Оптимизированная версия такой стратегии (вызов по необходимости) используется Haskell. Это так называемые «ленивые» вычисления.
  4. Вызов по значению. Здесь сокращение начинается с самого левого (внешнего) редекса, у которого в правой части стоит значение — замкнутый терм, который нельзя вычислить далее.

    Для чистого лямбда-исчисления таким термом будет λ-абстракция (функция), а в более богатых исчислениях это могут быть константы, строки, списки и т.п. Данная стратегия используется в большинстве языков программирования, когда сначала вычисляются все аргументы, а затем все вместе подставляются в функцию.

Если в терме больше нет редексов, то говорят, что он вычислен, или находится в нормальной форме. Не каждый терм имеет нормальную форму, например (λx.xx)(λx.xx) на каждом шаге вычисления будет порождать самоё себя (здесь первая скобка — анонимная функция, вторая — подставляемое в неё на место x значение).

Недостатком стратегии вызова по значению является то, что она может зациклиться и не найти существующее нормальное значение терма. Рассмотрим для примера выражение

(λx.λy. x) z ((λx.x x)(λx.x x))

Этот терм имеет нормальную форму z несмотря на то, что его второй аргумент такой формой не обладает. На её-то вычислении и зависнет стратегия вызова по значению, в то время как стратегия вызова по имени начнёт с самого внешнего терма и там определит, что второй аргумент не нужен в принципе. Вывод: если у редекса есть нормальная форма, то «ленивая» стратегия её обязательно найдёт.

Ещё одна тонкость связана с именованием переменных. Например, терм (λx.λy.x)y после подстановки вычислится в λy.y. Т.е. из-за совпадения имён переменных мы получим функцию тождества там, где её изначально не предполагалось. Действительно, назови мы локальную переменную не y, а z — первоначальный терм имел бы вид(λx.λz.x)y и после редукции выглядел бы как λz.y. Для исключения неоднозначностей такого рода надо чётко отслеживать, чтобы все свободные переменные из начального терма после подстановки оставались свободными. С этой целью используют α-конверсию — переименование переменной в абстракции с целью исключения конфликтов имён.

Так же бывает, что у нас есть абстракция λx.t x, причём x свободных вхождений в тело t не имеет. В этом случае данное выражение будет эквивалентно просто t. Такое преобразование называется η-конверсией.

На этом закончим вводную в лямбда-исчисление. В следующей статье мы займёмся тем, ради чего всё и затевалось: программированием на λ-исчислении.

Список источников

  1. «What is Lambda Calculus and should you care?», Erkki Lindpere
  2. «Types and Programming Languages», Benjamin Pierce
  3. Вики-конспект «Лямбда-исчисление»
  4. «Учебник по Haskell», Антон Холомьёв
  5. Лекции по функциональному программированию

Понравилась статья? Поделить с друзьями:
  • Как найти определенные слова в книге
  • Tvc это в экономике как найти
  • Как найти арабские цифры в телефоне
  • Как составить дополнение к письму
  • Как исправить отрицательный развал колес