Процедура Haskell

Question

module Algorithm where 

import System.Random 
import Data.Maybe 
import Data.List 

type Atom = String 
type Literal = (Bool,Atom) 
type Clause = [Literal] 
type Formula = [Clause] 
type Model = [(Atom, Bool)] 
type Node = (Formula, ([Atom], Model)) 

-- This function takess a Clause and return the set of Atoms of that Clause. 
atomsClause :: Clause -> [Atom] 


-- This function takes a Formula returns the set of Atoms of a Formula 
atoms :: Formula -> [Atom] 


-- This function returns True if the given Literal can be found within 
-- the Clause. 
isLiteral :: Literal -> Clause -> Bool 


-- this function takes a Model and an Atom and flip the truthvalue of 
-- the atom in the model 
flipSymbol :: Model -> Atom -> Model -- is this ok? 

Additional functions : 
remove :: (Eq a))a ->[a] ->[a] 
-This function removes an item from a list. 

neg :: Literal->Literal 
-This function flips a literal (ie. from P to :P and from :P to P). 
falseClause :: Model -> Clause -> Bool 
-This function takes a Model and a Clause and returns True 
if the clause is unsatisfied by the model or False otherwise. 
falseClauses :: Formula -> Model -> [Clause] 
-This function takes a Formula and a Model and returns the list of clauses of the formula that are not satisfied. 
assignModel :: Model -> Formula -> Formula 
-This function applies the assign function for all the assignments of a given model. 
checkFormula :: Formula -> Maybe Bool This function checks whether a formula can be decided to be satisfiable or unsatisfiable based on the effects of the assign function. 
satisfies :: Model -> Formula -. Bool This function checks whether a model satisfies a formula. This is done with the combination of the assignModel and checkFormula functions. 

Answer 1

Одно место, чтобы вы начали: смотреть на

removeTautologies :: Formula -> Formula 

Теперь предположим, что мы можем написать функцию

isTautology :: Clause -> Bool 

Тогда мы можем иметь возможность использовать эту функцию для фильтра общих формул , Поэтому я попытался бы игнорировать все, кроме функции isTautology. По существу здесь вопрос: Что такое тавтология и Как мы ее обнаружим? Некоторые идеи, опубликованные Эдвардом З. Янгом, должны определенно помочь вам понять, что происходит. В этом случае мы могли бы взглянуть на пункт [(True,"A"), (True,"B"), (False,"A")] и попытаться передать его isTautology для его тестирования. Аналогично с другой статьей, опубликованной Эдвардом, [(True,"B"), (True,"C"), (True,"A")].

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

Надеюсь, это поможет вам начать с вашей проблемы. Это может показаться совершенно неуместным, но обратите внимание, что в алгоритмах проверки модели используются более сложные варианты, которые подтверждают правильность вашего процессора, что ведут себя протоколы, а также недавно были использованы в автоматическом рефакторинге, см. http://coccinelle.lip6.fr/ для использования , Таким образом, эта проблема - хороший способ узнать серьезную применимость в реальном мире!

---

Я отредактирую его здесь, чтобы помочь вам, а не отвечать в разделе комментариев. Вы писали:

rt ((x, x') : (y, y') : rest) | x' == y' = rt rest 
           | otherwise = (x, x') : rt ((y, y') : rest) 

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

isRemovableClause :: Clause -> Bool 

Путь, который вы приняли требует от вас, чтобы отсортировать список в статье лексикографически, а затем рассмотрим, что делать в случае, если у вас есть [P, P, not P, Q], например. Другой подход - установить поиск. Предположим, что мы имеем

isRemovableClause ((tv, name) : rest) = ... 

Обратите внимание, что если значение (not tv, name) присутствует в rest это положение должно быть тавтологией. В противном случае мы можем выбросить (tv, name) и искать тавтологию в rest.

Перемещение фокуса на removeTautologies, то ясно, что функция может быть записана с помощью isRemovableClause: формула представляет собой список статей, поэтому мы можем просто пройти через п-списка и удалить все те, для которых isRemovableClause возвращает истину. Для достижения этой цели смелый решатель будет использовать List.filter, функцию более высокого порядка.

Answer 2

Этот вопрос слишком широк: это может быть немного ОК, если вы сосредоточились на одной конкретной функции, в которой вам нужна помощь, но на самом деле, для того чтобы мы могли эффективно, вам нужно дать нам больше, чем просто спецификация того, что код должен: только с этим, это просто проблема «Моя домашняя работа для меня».

Это, как говорится, я рекомендую брать примеры вы размещены в описаниях и их преобразования в вашем представлении (я предполагаю, что вы используете CNF?) Тогда вы будете иметь что-то вдоль линий

(A v B v -A)^(B v C v A) 

становится

[[(True,"A"), (True,"B"), (False,"A")], 
[(True,"B"), (True,"C"), (True,"A")]] 

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