non-termination

9зной

1ответ

Доказательство False с отрицательными индуктивными типами в Coq

В третьей главе CPDT кратко обсуждается, почему отрицательные индуктивные типы запрещены в Coq. Если бы мы имели Inductive term : Set := | App : term -> term -> term | Abs : (term -> term) -> term.

2зной

3ответ

Договор о домене Prolog: Как я могу узнать, какие вопросы вернут конечное число ответов?

Скажем, у меня есть пролог программа для объединения списков, как это: concat([],X,X). concat([Head|Tail],X,[Head|R]) :- concat(Tail,X,R). Как я могу знать, какие вопросы будут возвращать конечное

4зной

1ответ

Найти путь и его длину между узлами в графе

Я пытаюсь решить эту проблему, и я уже прочитал ответ this, но моя проблема связана с циклом infinte, даже если я использовал список посещенных узлов. Давайте посмотрим, мои две попытки: edge(1,2). e

3зной

2ответ

Преобразование предложения создает бесконечный цикл - но как?

Я не могу понять, где это происходит. Обратите внимание, что я очень новичок в Prolog, и я уверен, что у меня что-то не хватает - просто не знаю, что это может быть. Может ли кто-нибудь помочь мне, по

2зной

1ответ

Запрос не возвращается

Я пытаюсь выполнить какое-либо упражнение - представлять числа в «представлении», что означает, что «0» равно нулю, s (0) равно 1, s (s (0)) равно 2 и так далее , Я попытался написать предикат для доб

5зной

2ответ

Пролог-предикат - бесконечный цикл

Мне нужно создать предикат Пролога для мощности 2, с натуральными числами. натуральные числа: 0, s (0), s (s (0)) анс так далее .. Например: ?- pow2(s(0),P). P = s(s(0)); false. ?- pow2(P,s(s(0))).