Програмісти часто стикаються з проблемами читання математичних нотацій, коли намагаються розібратися з теоретичними основами будь-якої мови програмування. Також з ними штовхнувся і я в своїх теоретичних вишукуваннях. На щастя, мені дуже допомогла чудова стаття Джеремі Сіека (Jeremy Siek), чиїм перекладом я хочу з вами поділитися. Сподіваюся вона допоможе багатьом програмістам - «не математикам».
Вступ
Цим постом я хочу допомогти моїм друзям з читанням інших моїх постів. Це прискорений курс за нотаціями, що використовуються в теорії мов програмування (ТЯП). Для набагато кращого вивчення теми я рекомендую «Types and Programming Languages» від Benjamin C. Pierce і «Semantic Engineering with PLT Redex» від Felleisen, Findler, and Flatt. Я припускаю, що читач досвідчений програміст, але не такий хороший в математиці і ТЯП. Я почну з базових визначень і спробую швидко ввести вас в курс справи.
Безлічі, кортежі, стосунки та визначення правил
Я підозрюю, що багато читачів будуть знайомі з безліччями, кортежами і відносинами, але якщо ви не знайомі з індуктивними визначеннями, тоді прочитайте секцію нижче «визначення правилами».
Безлічі
Основний будівельний блок, який ми використовуємо в ТЯП - це безліч, тобто колекція об'єктів (або елементів). Наприклад, безліч, що складається з перших трьох натуральних чисел: {0, 1, 2}.
Єдиний факт, що має значення, це чи належить об'єкт безлічі чи ні. Не важливо, чи є дублікати або який порядок появи об'єкта в безлічі. Наприклад, безліч {0, 2, 1}, також безліч, що і наведене зверху. Нотація ∈ означає «в». Таким чином, 1 ∈ {0, 1, 2} істина і 3 ∈ {0, 1, 2} брехня. Безлічі можуть містити нескінченну кількість елементів. Наприклад, безліч всіх натуральних чисел (неотрицьових цілих), що позначається N.
Кортежі
Інший будівельний блок - це кортеж, тобто впорядкована колекція об'єктів. Тобто (0, 1, 2) є кортежем з трьох елементів і він відрізняється від кортежу (0, 2, 1). Підрядкова нотація ti означає i-й (з індексом i) елемент кортежу t. Наприклад, якщо t = (0, 2, 1), тоді t1 = 0, t2 = 2, t3 = 1. Кортежі завжди містять кінцеву кількість елементів і зазвичай досить небагато. Іноді для позначення кортежів використовуються кутові дужки замість круглих: .
Стосунки
Комбінуючи кортежі і безлічі ми отримуємо відносини. Ставлення - це безліч кортежів.
{(0, 1), (1,2), (2, 3), (3, 4), …}
Ми часто використовуємо стосунки для відображення вхідних значень на вихідні. Наприклад, ми можемо думати про ставлення вище як про відображення натурального числа на його послідовника, тобто на наступне більше натуральне число. Визначення зверху досить неточне через використання (...). На щастя, є більш точні нотації для опису нескінченних безліч і відносин.
Визначення правил
Основний спосіб, яким ми визначаємо нескінченні безлічі в ТЯП - надаємо набір правил, що описують, які елементи входять в безліч. Давайте використовуємо ім'я R для багатьох зверху. Тоді два наступних правила дадуть нам точне визначення R. Зверніть увагу, що друге правило рекурсивне в тому сенсі, що посилається на саме себе. Це нормальна і досить поширена ситуація.
- (0, 1) ∈ R.
- Для будь- яких натуральних чисел n і m, якщо (n, m) ∈ R, то (n + 1, m + 1) ∈ R.
Коли ми використовуємо правила для визначення безлічі, ми передбачаємо, що елемент не входить в безліч, якщо немає способу використовувати ці правила, щоб виправдати знаходження цього елемента в безлічі. Так (0, 0) не входить до R, тому що за допомогою зазначених правил не можна обґрунтувати, що (0, 0) туди входить.
Деякі набори правил безглузді і не визначають безліч. Наприклад, правила не повинні суперечити один одному, як тут:
- (0, 1) ∈ R.
- (0, 1) ∉ R.
Підручник з ТЯП описує обмеження для «хороших» наборів правил, але ми не будемо в це заглиблюватися. Скажімо тільки, що хоча б одне правило має бути нерекурсивним і подібні логічні протиріччя повинні бути відсутніми.
Загальнопоширена нотація для правил, як вище, використовує горизонтальну межу між «if» і «then». Наприклад, еквівалентне визначення для R дається наступним чином:
Ми опустили «для будь-яких натуральних чисел n і m» з правила 2. Використовується угода, згідно з якою змінні, такі як n і m, які з'являються в правилі, можуть бути замінені будь-яким об'єктом коректного типу. У даному випадку натуральним числом. Часто, «коректний тип», це щось про що можна здогадатися з контексту бесіди. У даному випадку - натуральні числа.
Припустимо, я стверджую, що певний елемент входить до R. Скажімо, (2, 3) ∈ R. Ви можете відповісти, що не вірите мені. Щоб вас переконати, мені потрібно показати, як правила виправдовують, той факт, що (2, 3) ∈ R. Я повинен показати вам висновок. Висновок - це ланцюжок правил, в якому змінні, такі як n і m, замінюються конкретними значеннями і передумови, такі як (n, m) ∈ R, замінюються більш конкретними висновками.
Я помітив кожен крок у виведенні номером правила. Химерна назва для того, що я називаю «визначення правилами» - індуктивне визначення.
Синтаксис мови та граматики
Виявляється, що використання правил для визначення багатьох, як ми робили вище, підходить і для визначення синтаксису мови програмування. Припустимо, що нам потрібно визначити просту мову для цілочисельної арифметики. Назвемо його Arith. Він буде містити вирази, такі як 1 + 3 і - (5 + 2). Згадаймо, що Z - безліч цілих чисел. Тоді безліч правил, що описують Arith, буде таким:
- Для будь-якого i ∈ Z вірно, що i ∈ Arith.
- Для будь-якого e, якщо e ∈ Arith, тоді -e ∈ Arith.
- Для будь-якого e1 і e2, якщо e1 ∈ Arith і e2 ∈ Arith, тоді e1 + e2 ∈ Arith.
- Для будь-якого e, якщо e ∈ Arith, тоді (e) ∈ Arith.
Бекуса-Наура форма (БНФ) - інша поширена нотація для запису правил, що визначають синтаксис мови, яка означає те саме. (Існує кілька варіантів БНФ. Я забув, яку саме використовую тут.) Набір правил називається граматикою.
Arith ::= integer
Arith ::= ""-"" Arith
Arith ::= Arith ""+"" Arith
Arith ::= ""("" Arith "")"
Вертикальна риса (що означає «або») часто використовується для того, щоб зробити синтаксис більш коротким.
Arith ::= integer | ""-"" Arith | Arith ""+"" Arith | ""("" Arith "")"
У ТЯП ми використовуємо своєрідний варіант БНФ, який замінює ім'я визначеної мови, в даному випадку Arith, на змінну, яка використовується для проходу за елементами Arith. Тепер припустимо, що використовуємо змінну i як заповнювач (placeholder) для цілих чисел і e як заповнювач для елементів Arith. Тоді ми можемо записати нашу граматику так:
e ::= i ∣ −e ∣ e + e
Зверніть увагу, що я опустив дужки. Зазвичай зрозуміло, що дужки дозволені в будь-якій мові. Поняття виводу збігається з деревом розбору (parse tree). Вони обидва демонструють, чому конкретний елемент входить у безліч.
Операційна семантика
Описати мову, значить описати, що станеться при запуску програми цією мовою. Саме це робить операційна семантика. У випадку з Arith нам потрібно вказати цілочисельний результат для кожної програми. Як було сказано вище, ми можемо використовувати відносини для відображення вхідних даних на результат. І зазвичай ми так і робимо в ТЯП. Є кілька різних стилів відносин. Перший, який ми розглянемо, це семантика великого кроку (big-step semantics), яка відображає програму прямо на її результат.
Семантика великого кроку (big-step semantics)
Визначте відношення Eval, яке відображає елементи Arith на цілі числа. Наприклад, має виконуватися умова (‑ (2 + ‑ 5), 3) ∈ Eval. Це ставлення буде нескінченним (тому що існує нескінченна кількість програм на Arith). І знову ми будемо використовувати набір правил для визначення Eval. Але перед тим як ми почнемо, введемо скорочення: означає (e, i) ∈ Eval. Нижче ми опишемо правила, що визначають Eval з використанням нотації з горизонтальною рисою. Щоб переконатися, що не пропустимо жодної програми, створимо одне правило для кожного синтаксичного правила Arith (їх три). Будемо говорити, що правила синтаксично-орієнтовані, коли одне правило відповідає кожному синтаксичному правилу мови.
Це може здатися трохи дивним, що я визначив «» - «» в термінах «» - «» і «» + «» в термінах «» + «». Чи не циклічна це залежність? Відповідь - ні. Плюс і мінус - це звичайні арифметичні операції для цілих чисел, які кожен проходить у школі. У цьому сенсі більш дивним для Arith було б не використовувати 32 або 64-бітну арифметику. Програміст, який реалізує Arith, міг би використовувати пакет для роботи з BigInteger, щоб обробляти арифметику.
Семантика малого кроку (small-step semantics)
Другий і найбільш поширений стиль операційної семантики - це семантика малого кроку. У цьому стилі відношення не відображає програму на її результат. Замість цього воно відображає програму на злегка спрощену програму, в якій якесь подвираження замінюється його результатом. Можна думати про цей стиль, як про текстову заміну. Щоб дати приклад цього стилю, визначимо ставлення Step. Це відношення буде містити такі елементи, як і багато інших:
(-(2 + -5), -(-3)) ∈ Step
(-(-3), 3) ∈ Step
Знову введемо скорочення: означає (e1, e2) ∈ Step. І якщо ми з'єднаємо кроки разом, то буде означати і. Синонімом для кроку (step) буде термін «скоротити» (reduce). Попередній приклад з двох кроків може бути записаний тепер так:
Тепер перейдемо до правил, що визначають ставлення Step. Тут п'ять правил, які ми пояснимо нижче.
Правила (1) і (2) найцікавіші. Вони виконують арифметику. Ми називаємо їх «обчислювальні правила скорочення» (computational reduction rules). Правила (3-5) дозволяють нам заходити в подвираження для виконання обчислень. Вони часто називаються правилами відповідності (congruence rules) з причин, у які ми зараз не будемо вдаватися. Використання змінної i в правилі (5) означає, що скорочення відбувається зліва направо. Зокрема, ми не дозволяємо скорочувати правий вираз від знака + до тих пір, поки лівий вираз не буде скорочено до цілого числа.
Відступ: Розглянутий тут порядок «зліва направо» я вибрав як дизайнер мови. Я міг би не визначати порядок, дозволяючи бути йому невизначеним. Наша мова не має побічних ефектів, тому порядок не має значення. Однак, більшість мов мають побічні ефекти і вони визначають порядок (але не всі), тому я подумав, що потрібно розглянути приклад того, як зазвичай визначає порядок.
Час для прикладу. Подивимося на висновок для кроку:
Ми визначили один крок обчислень, тобто відносини Step. Але ми не зовсім закінчили. Ми ще повинні визначити, що означає виконати програму до завершення. Ми зробимо це за допомогою визначення Eval'в термінах відносини Step. Іншими словами, відношення Eval'буде містити будь-які пари (e, i) якщо вираз e скорочується до цілого i за нуль або більше кроків. Тут присутня нова нотація, яка пояснюється далі.
Нотація {... ∣...} визначає конструктор множини. Вираз ліворуч від вертикальної межі визначає шаблон для типового елемента множини і вираз праворуч - обмеження на елементи безлічі. Нотація означає нуль або більше кроків. Я б визначив ці багатошагові відносини за допомогою правил:
(Я думаю про це в термінах Lisp-подібних списків. Так, першому правилу відповідає nil, а другому cons.)
Системи типів (з лямбда-обчисленням як приклад)
Багато мов програмування статично типізовані, тобто компілятор виконує деякі перевірки коректності перш, ніж виконати реальну компіляцію. Зазвичай, під час перевірки компілятор переконується в тому, що об'єкти використовуються так, як повинні. Наприклад, ніхто не намагається використовувати ціле число як функцію. Спосіб, яким розробник мови вказує які саме перевірки мають бути виконані, є визначення системи типів для мови. Мова Arith настільки проста, що в ній немає ніяких цікавих перевірок типів. Розглянемо більш складну мову, яка знову і знову використовується в ТЯП - лямбда-обчислення (технічно, лямбда-обчислення зі спрощеною типізацією). Лямбда-обчислення складається тільки з анонімних функцій. Ми ж розширимо лямбда-обчислення так, щоб воно включало наші арифметичні вирази. Тоді наша мова буде визначатися наступною граматикою.
e ::= i ∣ −e ∣ e + e ∣ x ∣ e e ∣ λx:T.e
Змінна x перераховує назви параметрів, такі як foo та g. Наступні праворуч два вирази (e e) означають застосування функції (або виклик функції). Якщо ви знайомі з мовою C, можете читати e1 e2 як e1 (e2). У лямбда-обчисленні функції приймають тільки один параметр, тому виклик функції вимагає тільки один аргумент. Синтаксис x:T.e створює функцію з одним параметром x типу T (типи ми скоро визначимо) і тілом, що складається з виразу e. (Часто люди помиляються думаючи, що x - це ім'я функції. Насправді це назва параметра, оскільки функції є анонімними, тобто не мають імені.) Поверненим значенням функції буде результат виразу e. Тепер подумаємо про те, які об'єкти будуть існувати під час виконання програми. Це цілі числа і функції. Ми створимо безліч типів для опису сортів об'єктів, використовуючи T для перерахування безлічі типів.
У функціональному типі T1 є типом параметра, а T2 типом значення, що повертається.
Робота системи типів полягає в тому, щоб прогнозувати, який тип значення буде у результату виразу. Наприклад, вираз - (5 + 2) повинен мати тип Int, тому що результат - (5 + 2) - це число -3, яке є цілим. Також як у разі визначення синтаксису або операційної семантики мови, ТЯП-теоретик використовує відносини і правила для визначення системи типів. Ми визначимо ставлення WellTyped, яке, в першому наближенні, відображає вирази на типи. Наприклад, буде виконано (- (5 + 2), Int) ∈ WellTyped.
Однак, оскільки лямбда-обчислення включає змінні, ми потребуємо якогось аналогу таблиці символів, відношення, званому оточенням типів (type environment), для відстеження які змінні мають який тип. Грецька літера - це гама, яка зазвичай використовується для цієї мети. Ми повинні бути здатні створити нове оточення типів зі старого, з можливістю приховувати змінні із зовнішніх областей видимості. Щоб визначити математичний апарат для цих можливостей, покладімо, що Γ∖x буде ставленням, таким же як ^, за винятком того, що будь-який кортеж, що починається з x буде виключений. (Залежно від способу, яким буде визначено систему типів, може бути 0 або 1 кортеж, який починається з x, роблячи оточення типів спеціальним видом ставлення, званого часткова функція (partial function). Ми будемо писати, x:T для дії розширення середовища типів за допомогою змінної x, можливо, перевизначає попереднє визначення, і визначене наступним чином:
Припустимо, що
Тоді
Оточення типів відрізняється від глобальної таблиці символів у компіляторі тим, що може існувати більше одного середовища типів, по одному для кожної області видимості. Крім того, ми не оновлюємо оточення типів, замість цього ми створюємо нове оточення, яке злегка відрізняється від старого. З точки зору програмування, математична метарама, яку ми тут використовуємо, є чистою функціональною (pure functional), тобто вона не містить побічних ефектів. Читач може турбуватися про те, що це веде до неефективності, але згадайте, що ми не пишемо тут програму, ми пишемо специфікацію! Найбільше значення для нас має зрозумілість. І залишаючись чистими ми можемо писати більш зрозумілі речі.
Повертаючись до відношення WellTyped, замість того, щоб містити кортежі з двох елементів (2-кортежі, пари) воно буде містити кортежі з трьох елементів (3-кортежі, трійки) виду (^, e, T). Таким чином ми приписуватимемо типи виразів у контексті оточення типів. Введемо ще одне скорочення (ТЯП-теоретики люблять скорочення!). Будемо писати замість (^, e, T) ∈ WellTyped. Тепер ми готові перерахувати правила, що визначають WellTyped.
Підіб'ємо підсумок для правил вище. Арифметичні оператори працюють з цілими числами. Змінні отримують свої типи з середовища. Лямбди є функціональними типами, заснованими на типі їх параметра і типі результату. Тіло лямбди перевірено за допомогою оточення з точки створення (lexical scoping), розширеного за допомогою параметра цієї лямбди. І застосування функції не порушує логіки мови до тих пір, поки тип аргументу збігається з типом параметра.
Ув'язнення
На цьому закінчується цей прискорений курс за нотаціями, що використовуються в теорії мов програмування. Цей пост тільки описує основи, але дуже багато додаткових нотацій, які вам знадобляться, є варіаціями розглянутих тут. Щасливого читання і не соромтеся ставити запитання в коментарях.
