Существует ли Пролог более высокого порядка, которому не нужна система типов?

Question

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

Существуют ли альтернативные прологи более высокого порядка, которым не нужны файлы .sig?
Может быть, с помощью гораздо более простой системы типов, которая не требует такого количества
объявлений, но все же имеет некоторую форму унификации более высокого порядка?

Можно ли решить эту дилемму?

Answer 1

Существует ли Пролог более высокого порядка, которому не нужна система типов?

Это бестиповые:

• HiLog

• Привет Орд

Из статьи HiOrd:

Предлагаемая структура вызывает много вопросов, которые авторы надеются решить в будущих исследованиях. В частности, необходимо разработать строгую обработку для сравнения с другими формальными системами более высокого порядка (Hilog, Lambda-Prolog). Например, достаточно просто консервативно перевести фрагмент Хорна более высокого порядка из λProlog в Hiord путем стирания типов, поскольку правила разрешения, по существу, те же самые (предполагая безопасную для типов процедуру унификации более высокого порядка).

• Чао (включая HiOrd)