Skip to content

Commit 1ddb483

Browse files
author
Marat Zimnurov
committed
Rosetta Code: семь канонических задач, и граница языка сторожится тестом
Витрина, где язык сравнивают не с обещаниями, а с тем же решением на сорока других языках. Поэтому важнее краткости то, что видно на просмотре: где завершение доказано, а где язык честно говорит, что не может. Два решения переписаны на форму «разложить … на символы», и это тот случай, ради которого форма и заводилась. Обращение строки и палиндром объясняли в шапках, ПОЧЕМУ посимвольный проход недоказуем: разбор образцом работает только со списком, у строки хвоста нет, обход шёл по позиции — убывало число, а не значение. Теперь строка раскладывается в список, и оба файла тотальны целиком: 4 из 4 и 14 из 14 вместо 3 из 6 и 12 из 15. Три решения тотальными не стали, и это записано, а не спрятано. «Числа от и до» рекурсирует по числу: счёт до N завершается очевидно человеку, но обосновать это компилятор может только рассуждением о натуральных числах, которого не ведёт. Быстрая сортировка рекурсирует по отфильтрованным подспискам — подсписок меньше исходного, но не является его хвостом. Обе границы названы в шапках. Тест сверяет не только запуск и примеры, но и ЧИСЛО тотальных функций в каждом файле. Не ради числа: набор показывает границу языка, и сдвинься она — тексты в шапках станут враньём. Ровно это уже произошло однажды, когда появилась новая встроенная форма, и заметить такое обязан тест, а не читатель. README перечисляет и то, что не выражается вовсе: задачи с вводом-выводом, задачи с функциями как значениями и задачи о бесконечных последовательностях. Список короткий и про устройство языка, а не про «не успели».
1 parent e9763e9 commit 1ddb483

9 files changed

Lines changed: 1034 additions & 0 deletions

File tree

flang/examples/rosetta/README.md

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
# Rosetta Code на flang
2+
3+
Канонические задачи, решённые на языке. Rosetta Code — витрина, где язык
4+
сравнивают не с обещаниями, а с тем же решением на сорока других языках,
5+
поэтому здесь важнее не краткость, а то, что видно на просмотре: где язык
6+
доказывает завершение, а где честно говорит, что не может.
7+
8+
Каждый файл запускается. Прогон — `flang/test/rosetta.test.mjs`; он проверяет
9+
разбор, типы, завершаемость, все примеры и, сверх того, **число тотальных
10+
функций**. Последнее не ради числа: набор показывает границу языка, и если она
11+
сдвинется, объяснения в шапках файлов станут враньём — заметить это обязан
12+
тест, а не читатель.
13+
14+
| Задача | Файл | Тотальных | Чем интересна на flang |
15+
|---|---|---|---|
16+
| Reverse a string | `reverse-string.flang` | 4 из 4 | обращение строки доказуемо завершается, и по кодовым точкам — эмодзи не разваливается |
17+
| Palindrome detection | `palindrome.flang` | 14 из 14 | нормализация и сравнение целиком доказаны; отдельно показана та же задача на списке |
18+
| Merge sort | `merge-sort.flang` | 8 из 8 | слияние доказывается: рекурсия идёт по хвостам обоих списков |
19+
| Quicksort | `quicksort.flang` | 4 из 5 | сама сортировка **не** доказывается — рекурсия по отфильтрованным подспискам, а подсписок не хвост |
20+
| FizzBuzz | `fizzbuzz.flang` | 3 из 5 | классика, на которой видно, что счёт до N в этом языке не бесплатен |
21+
| Factorial | `factorial.flang` | 2 из 5 | то же: `Числа от и до` рекурсирует по числу |
22+
| Fibonacci | `fibonacci.flang` | 2 из 6 | и шаговый вариант, и ряд — оба упираются в счёт |
23+
24+
## Почему часть решений не тотальна
25+
26+
Это не недоделка, а граница, которую язык проводит осознанно.
27+
28+
Тотальность доказывается **структурным убыванием**: каждый рекурсивный вызов
29+
обязан получать структурно меньший аргумент — хвост списка, поле записи, поле
30+
варианта. Убывание числа таковым не считается. `«Числа от и до» от 1 и n`
31+
очевидно завершается человеку, но обосновать это компилятор может только
32+
рассуждением о натуральных числах, которого он не ведёт.
33+
34+
Так же с быстрой сортировкой: `отфильтровать` даёт новый список, и он
35+
**меньше** исходного — но не является его хвостом, а значит структурного
36+
убывания нет.
37+
38+
Обе границы названы прямо в шапках соответствующих файлов. Заявлять «язык, где
39+
всё доказано» и молчать о таких случаях было бы ровно тем, против чего язык и
40+
затевался.
41+
42+
## Что пока не выражается вовсе
43+
44+
Список честный и короткий; он не про «не успели», а про устройство языка.
45+
46+
**Задачи с вводом-выводом** — «прочитать файл», «запросить страницу», «спросить
47+
у пользователя». Язык чистый: эффект выражается описанием действия, которое
48+
исполняет хозяин, а монады ввода-вывода пока нет. На flang пишется то, что с
49+
данными делают, не то, как их достают.
50+
51+
**Задачи, требующие функций как значений** — «отсортировать заданным
52+
компаратором», «свернуть переданной операцией», комбинаторы. Функции не
53+
являются значениями первого класса: это плата за прямую печать в восемь языков
54+
и за разрешимый анализ завершаемости.
55+
56+
**Задачи о бесконечных последовательностях** — «первые N простых ленивым
57+
решетом». Ленивости нет, а конечное приближение — уже другая задача, и выдавать
58+
одно за другое на витрине нечестно.
59+
60+
## Как это выложить
61+
62+
Разметка Rosetta Code — своя вики. Заголовок языка и блок кода:
63+
64+
```
65+
=={{header|flang}}==
66+
Обращение строки доказуемо завершается: строка раскладывается в список
67+
символов, дальше идёт свёртка по готовому списку.
68+
<syntaxhighlight lang="text">
69+
тотальная функция «Обратить строку»
70+
принимает текст: строка
71+
возвращает строка
72+
свёртка (разложить текст на символы) начиная с "" как акк и буква
73+
→ соединить буква с акк
74+
</syntaxhighlight>
75+
```
76+
77+
`lang="text"` намеренно: своего лексера у Rosetta Code для flang нет, а чужой
78+
раскрасит слова неверно и собьёт с толку сильнее, чем отсутствие цвета.
Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
модуль «Факториал»
2+
3+
// Rosetta Code — Factorial.
4+
// n! = 1·2·…·n, причём 0! = 1. Задача просит и рекурсивный вариант, и
5+
// итеративный.
6+
//
7+
// В flang эти два варианта различаются не стилем, а классом функции, и это
8+
// самое интересное, что тут можно показать.
9+
//
10+
// Итеративный — это произведение списка [1..n], то есть свёртка. Свёртка
11+
// обходит готовый список ровно один раз, поэтому «Произведение» тотальна:
12+
// компилятор доказал, что она завершается.
13+
//
14+
// Рекурсивный — «n умножить на факториал от n−1». Убывает число, а про
15+
// результат арифметики анализ завершаемости не знает ничего (SPEC, раздел 1:
16+
// частью значения считаются хвост списка, голова, поле записи и поле
17+
// варианта). Пометить такую функцию `тотальная` — получить FLANG_NOT_TOTAL,
18+
// и подгонять тут нечего: это ровно та рекурсия, которую язык сознательно
19+
// не доказывает.
20+
//
21+
// Ту же цену платит и «Числа от и до»: список [1..n] тоже приходится
22+
// насчитывать счётчиком. Поэтому тотальна здесь именно та часть, где данные
23+
// уже есть, — и это общее правило языка, а не особенность факториала.
24+
25+
тотальная функция «Приписать в начало»
26+
принимает первое: число, элементы: список числа
27+
возвращает список числа
28+
пример «В пустой»
29+
дано первое равно 1
30+
дано элементы равно пустой список
31+
ожидается [1]
32+
свёртка элементы начиная с [первое] как акк и эл → добавить эл к акк
33+
34+
тотальная функция «Произведение»
35+
принимает элементы: список числа
36+
возвращает число
37+
пример «Произведение четырёх»
38+
дано элементы равно [1, 2, 3, 4]
39+
ожидается 24
40+
пример «Произведение пустого — единица»
41+
дано элементы равно пустой список
42+
ожидается 1
43+
свёртка элементы начиная с 1 как акк и эл → акк умножить на эл
44+
45+
// ─────────────────────────────────────────────────────────────────────────
46+
// Дальше — обычные функции: рекурсия по числу.
47+
// ─────────────────────────────────────────────────────────────────────────
48+
49+
функция «Числа от и до»
50+
принимает начало: число, конец: число
51+
возвращает список числа
52+
пример «От одного до пяти»
53+
дано начало равно 1
54+
дано конец равно 5
55+
ожидается [1, 2, 3, 4, 5]
56+
пример «Пустой промежуток»
57+
дано начало равно 1
58+
дано конец равно 0
59+
ожидается пустой список
60+
если начало больше конец
61+
то пустой список
62+
иначе «Приписать в начало» от начало и («Числа от и до» от (начало плюс 1) и конец)
63+
64+
// Итеративный вариант из условия задачи: произведение промежутка.
65+
функция «Факториал произведением»
66+
принимает н: число
67+
возвращает число
68+
пример «Пять факториал»
69+
дано н равно 5
70+
ожидается 120
71+
пример «Ноль факториал»
72+
дано н равно 0
73+
ожидается 1
74+
«Произведение» от («Числа от и до» от 1 и н)
75+
76+
// Рекурсивный вариант из условия задачи.
77+
функция «Факториал»
78+
принимает н: число
79+
возвращает число
80+
пример «Пять факториал»
81+
дано н равно 5
82+
ожидается 120
83+
пример «Десять факториал»
84+
дано н равно 10
85+
ожидается 3628800
86+
пример «Ноль факториал»
87+
дано н равно 0
88+
ожидается 1
89+
пример «Двадцать факториал ещё точен в double»
90+
дано н равно 20
91+
ожидается 2432902008176640000
92+
если н не больше 1
93+
то 1
94+
иначе н умножить на («Факториал» от (н минус 1))
Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
модуль «Фибоначчи»
2+
3+
// Rosetta Code — Fibonacci sequence.
4+
// F(0) = 0, F(1) = 1, дальше сумма двух предыдущих. Нужны и отдельный член
5+
// ряда, и начало ряда списком.
6+
//
7+
// Отдельный член уже решён в `flang/examples/leetcode/509-fibonacci-number.flang`
8+
// и там же объяснено, почему он обычный: убывает счётчик, а убывание по числу
9+
// анализ завершаемости не признаёт. Здесь интересно другое — ряд.
10+
//
11+
// Ряд выражается свёрткой, а свёртка тотальна всегда: она обходит готовый
12+
// список и не может обойти его дважды. Значит вопрос только в том, откуда
13+
// взять список нужной длины. Если он у вызывающего уже есть — «Ряд по
14+
// топливу» тотальна, и это не уловка: длина ряда буквально равна длине
15+
// данных, по которым идёт свёртка. Если длину задают числом, впереди
16+
// неизбежно встаёт счётчик, и функция становится обычной.
17+
//
18+
// Приём с топливом стоит запомнить: в языке без циклов и без функций первого
19+
// класса «список нужной длины» — единственная форма ограниченного повторения,
20+
// которую компилятор умеет принять как доказательство.
21+
22+
объект «Состояние ряда»
23+
числа является список числа
24+
предыдущее является числом
25+
текущее является числом
26+
27+
тотальная функция «Приписать в начало»
28+
принимает первое: число, элементы: список числа
29+
возвращает список числа
30+
пример «В пустой»
31+
дано первое равно 1
32+
дано элементы равно пустой список
33+
ожидается [1]
34+
свёртка элементы начиная с [первое] как акк и эл → добавить эл к акк
35+
36+
// Столько членов ряда, сколько элементов в топливе. Тотальная: единственное
37+
// повторение — свёртка по готовому списку.
38+
тотальная функция «Ряд по топливу»
39+
принимает топливо: список числа
40+
возвращает список числа
41+
пример «Пять членов»
42+
дано топливо равно [0, 0, 0, 0, 0]
43+
ожидается [0, 1, 1, 2, 3]
44+
пример «Пустое топливо — пустой ряд»
45+
дано топливо равно пустой список
46+
ожидается пустой список
47+
пусть начальное равно запись «Состояние ряда» с числа равным пустой список и предыдущее равным 0 и текущее равным 1
48+
пусть итог равно свёртка топливо начиная с начальное как акк и шаг
49+
запись «Состояние ряда» с числа равным (добавить акк.предыдущее к акк.числа) и предыдущее равным акк.текущее и текущее равным (акк.предыдущее плюс акк.текущее)
50+
итог.числа
51+
52+
// ─────────────────────────────────────────────────────────────────────────
53+
// Дальше — обычные функции: там, где длину задаёт число, а не список.
54+
// ─────────────────────────────────────────────────────────────────────────
55+
56+
функция «Числа от и до»
57+
принимает начало: число, конец: число
58+
возвращает список числа
59+
пример «От одного до трёх»
60+
дано начало равно 1
61+
дано конец равно 3
62+
ожидается [1, 2, 3]
63+
если начало больше конец
64+
то пустой список
65+
иначе «Приписать в начало» от начало и («Числа от и до» от (начало плюс 1) и конец)
66+
67+
функция «Ряд Фибоначчи»
68+
принимает сколько: число
69+
возвращает список числа
70+
пример «Первые десять»
71+
дано сколько равно 10
72+
ожидается [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]
73+
пример «Ноль членов»
74+
дано сколько равно 0
75+
ожидается пустой список
76+
«Ряд по топливу» от («Числа от и до» от 1 и сколько)
77+
78+
функция «Фибоначчи шагом»
79+
принимает осталось: число, предыдущее: число, текущее: число
80+
возвращает число
81+
пример «Шагов не осталось»
82+
дано осталось равно 0
83+
дано предыдущее равно 7
84+
дано текущее равно 9
85+
ожидается 7
86+
если осталось не больше 0
87+
то предыдущее
88+
иначе «Фибоначчи шагом» от (осталось минус 1) и текущее и (предыдущее плюс текущее)
89+
90+
функция «Фибоначчи»
91+
принимает н: число
92+
возвращает число
93+
пример «Нулевой»
94+
дано н равно 0
95+
ожидается 0
96+
пример «Десятый»
97+
дано н равно 10
98+
ожидается 55
99+
пример «Сороковой»
100+
дано н равно 40
101+
ожидается 102334155
102+
«Фибоначчи шагом» от н и 0 и 1

0 commit comments

Comments
 (0)