Могут ли компиляторы вывести/доказать математически?

Ответ 1

Компиляторы обычно не пытаются автоматически доказывать эту вещь, потому что ее трудно реализовать.

Помимо добавления логики к компилятору для преобразования одного фрагмента кода в другой, вы должны быть очень осторожны, чтобы он только пытался сделать это, когда он действительно безопасен, т.е. часто существует множество "побочных условий" для беспокоюсь о. Например, в приведенном выше примере кто-то мог написать экземпляр класса типа Num (и, следовательно, оператора (+)), где a + b не b + a.

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

Например, и я не тестировал это, вы можете использовать следующее правило для одного из приведенных выше примеров:

{-# RULES
  "sum/reverse"    forall list .  sum (reverse list) = sum list
    #-}

Обратите внимание на круглые скобки вокруг reverse list - то, что вы написали в своем вопросе, на самом деле означает (sum reverse) list и не будет проверяться typecheck.

EDIT:

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

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

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

• FFTW - это пример библиотеки, которая делает все виды математической оптимизации внутренне. Некоторые из его кода сгенерированные настраиваемым компилятором, авторы писали специально для этой цели. Это стоит того, потому что у авторов есть знания об оптимизации, связанные с доменом, которые в конкретном контексте библиотеки стоят усилий и безопасности

• Люди иногда используют метапрограммирование шаблонов для написания "самооптимизирующихся библиотек", которые снова могут полагаться на арифметические идентификаторы, см., например, Blitz ++. Тодд Велдуйзен, доктор философии имеет хороший обзор.

• Если вы спускаетесь в царства игрушечных и академических компиляторов, все происходит. Например, моя собственная докторская диссертация посвящена написанию неэффективных функциональных программ наряду с небольшими сценариями, которые объясняют, как их оптимизировать. Многие из примеров (см. Главу 6) полагаются на применение арифметических правил для обоснования основополагающих оптимизаций.

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

Ответ 2

Ответ

Нет, компиляторы не делают такого рода вещи.

Одна из причин, по которым

И для ваших примеров это было бы даже неправильно: поскольку вы не указали аннотации типов, компилятор Haskell выберет наиболее общий тип, который будет

foldr (+) 0 [ 1 ..10]  :: Num a => a

и аналогичных

(\list -> sum (reverse list)) :: Num a => [a] -> a

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

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

Исключение

Примечание. Заметными исключениями являются линейные преобразования в циклах. Большинство компиляторов переписывают

for (int i = 0; i < n; i++) {
   ... 200 + 4 * i ...
}

к

for (int i = 0, j = 200; i < n; i++, j += 4) {
   ... j ...
}

или что-то подобное, поскольку этот шаблон часто встречается в коде, работающем над массивом.

Ответ 3

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

sum list == sum (reverse list)

Компилятор должен знать или принимать во внимание следующие факты:

• sum = foldl (+) 0
• (+) является коммутативным
• обратный список - это перестановка списка
• foldl x c l, где x является коммутативным и c является константой, дает тот же результат для всех перестановок l.

Все это кажется тривиальным. Конечно, компилятор, скорее всего, найдет определение sum и ввел его. Может потребоваться, чтобы (+) был коммутативным, но помните, что + - это просто еще один символ, не имеющий приложенного значения компилятору. Третий момент потребовал бы, чтобы компилятор доказал некоторые нетривиальные свойства около reverse.

Но дело в следующем:

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

• Вы все еще не можете заменить выражение выше True, если не можете исключить возможность того, что список или элемент списка внизу. Обычно этого нельзя делать. Вы даже не можете выполнить следующую "тривиальную" оптимизацию f x == f x во всех случаях

   f x `seq` True
  

Для рассмотрим

f x = (undefined :: Bool, x)

то

f x `seq` True    ==> True
f x == f x        ==> undefined

Говоря, что ваш первый пример слегка модифицирован для мономорфизма:

 f n = n * foldl (+) 0 [1..10] :: Int

можно оптимизировать программу, вытеснив выражение из его контекста и заменив его на имя константы, например:

const1 = foldl (+) 0 [1..10] :: Int
f n = n * const1

Это связано с тем, что компилятор может видеть, что выражение должно быть постоянным.

Ответ 4

То, что вы описываете, выглядит как суперкомпилирование. В вашем случае, если выражение имело тип monomorphic типа Int (в отличие от полиморфного Num a => a), компилятор мог бы сделать вывод, что выражение foldr (+) 0 [1 ..10] не имеет внешних зависимостей, поэтому его можно было бы оценить во время компиляции и заменить на 55. Тем не менее, AFAIK no mainstream компилятор в настоящее время делает такую ​​оптимизацию.

(В функциональном программировании "проверка" обычно ассоциируется с чем-то другим. В языках с зависимые типы типы являются достаточно мощными, чтобы выразить сложное предложение а затем через файлы Карри-Говарда становятся доказательствами таких предложений.)

Ответ 5

Как отмечали другие, неясно, что ваши упрощения даже держатся в Haskell. Например, я могу определить

newtype NInt = N Int
instance Num NInt where
  N a + _ = N a
  N b * _ = N b
  ... -- etc

а теперь sum . reverse :: Num [a] -> a не равно sum :: Num [a] -> a, так как я могу специализировать каждый на [NInt] -> NInt, где sum . reverse == sum явно не выполняется.

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

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

Итак, что требуется, чтобы \x -> sum [0..x] заменить на \x -> x*(x + 1)/2? Компилятору понадобится теория чисел и встроенная алгебра. Это невозможно в Haskell или ML, но становится возможным в зависимости от типизированных языков, таких как Coq, Agda или Idris. Там вы можете указать такие вещи, как

revCommute :: (_+_ :: a -> a -> a) 
            -> Commutative _+_ 
            -> foldr _+_ z (reverse as) == foldr _+_ z as

а затем, теоретически, скажите компилятору переписать в соответствии с revCommute. Это все равно будет сложно и сложно, но по крайней мере у нас будет достаточно информации. Чтобы быть ясным, я пишу что-то очень странное выше, зависимый тип. Тип зависит не только от возможности вводить как тип, так и имя аргумента inline, но также и весь синтаксис вашего языка "на уровне уровня".

Есть много различий между тем, что я только что написал, и тем, что вы сделали бы в Haskell. Во-первых, для того, чтобы сформировать базу, в которой такой promises можно воспринимать всерьез, мы должны отбросить общую рекурсию (и, следовательно, нам уже не нужно беспокоиться о проблемах без прекращения действия, таких как stream-fusion). У нас также должно быть достаточно структуры для создания чего-то вроде обещания Commutative _+_. Вероятно, это зависит от наличия целой теории операторов и математики, встроенной в языковую стандартную библиотеку, которую вам нужно будет создать самостоятельно. Наконец, богатство системы типов, требуемое для выражения таких теорий, добавляет большую сложность всей системе и выдает вывод типа, как вы его знаете сегодня.

Но, учитывая всю эту структуру, я никогда не смогу создать обязательство Commutative _+_ для _+_, определенное для работы на NInt, и поэтому мы можем быть уверены, что foldr (+) 0 . reverse == foldr (+) 0 действительно выполняется.

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

foldr (+) 0 . reverse
foldr (+) 0 (reverse as)

не совпадают. Они "очевидно" одинаковы из-за некоторых правил, которые мы могли бы доказать о (.), но это означает, что теперь компилятор должен вызывать два встроенных правила для выполнения нашей оптимизации.

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

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

Blech.

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

И он даже не стреляет. Для примера борьбы с этой проблемой рассмотрим источник Vector для всех прагм ПРАВИЛ, в которых указаны все распространенные обстоятельства, в которых следует оптимизировать оптимизацию потоков Vector.

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

Ответ 6

Интересный факт: учитывая две произвольные формулы, оба они дают одинаковый вывод для одних и тех же входных данных? Ответ на этот тривиальный вопрос не является вычислимым! Другими словами, математически невозможно написать компьютерную программу, которая всегда дает правильный ответ за конечное время.

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

Кроме того, разве это не работа программиста? Если вы хотите, чтобы сумма арифметической последовательности была достаточно достаточной, чтобы это было узким местом производительности, почему бы просто не написать более эффективный код самостоятельно? Аналогично, если вы действительно хотите числа Фибоначчи (почему?), Используйте алгоритм O (1).