Structural induction

Posted on August 6, 2019

Постигаю алгоритм Knuth-Bendix completion. Источники:


Proofs by Induction in Equational Theories with Constructors

есть множество Σ

Каждый оператор F в Σ задан с арностью (то есть F - функции)

Σ = C ∪ D где C - множество конструкторов (похоже CGT), D - defined operators (то есть заданные функции)

Предполагается что есть как минимум два конструктора (true/false)

Τ - множество термов, каждый из которых состоит из операторов(функций) из Σ и переменных из denumerable множества ν

G - множество ground terms (то есть термы без переменных) - непустое

GC - множество constructor ground terms (то есть термы созданные только из конструкторов)

Пусть ε - множество equations над Σ

=ε - соответствие (эквивалентность) на Τ

Тогда ε определяет D через C iff для каждого M в G существует уникальный N в GC такой что M =ε N

Что следует читать как:

У нас есть множество подстановок(эквивалентностей) такое что мы можем любой ground term сконвертировать в соотвествующий CGT (то есть тупо мы в состоянии производить вычисления) Если это так то: ε определяет D через C.