Почему срок переписывания?

Я сделал немного googleing и придумал немного меньше.

Мне интересно, каковы основные причины для ученых, программистов, изучать переписывание терминов и / или переписывание терминов графов.

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

Любая помощь будет наиболее ценится!

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

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

Так что это говорит о том, что системы переписывания в целом имеют много общего с алгоритмами выражения.

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

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

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

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

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

Я предлагаю вам взглянуть на статью в Википедии на эту тему .

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

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

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

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

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

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

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

Одним из примеров этой моей системы, DMS Software Reengineering Toolkit , который был использован для широкого спектра анализа программ и масштабных задач преобразования. Вы можете увидеть, как DMS выражает переписывает . Эти переписывания применяются ассоциативно-коммутативной системой переписывания терминов, которая работает за кулисами.