Задания лабораторной работы No.2 по курсу "Автоматическое доказательство теорем" доц. А.Л.Хижа кафедра компьютерных технологий, ФПМ, ДНУ 2011/2012 Тема ---- Программирование на ACL2 Лабораторная работа №2 ;; Часть 1: Чему равняется ; Для каждого из нижеприведенных выражений укажите, каково значение ; левой части равенства и замените символ # правильным значением. ; Должно получиться такое выражение, которое ACL2 не посчитает ошибочным. ; Например: ; ; (equal (/ 3 2) #) ; ; должно превратиться в выражение ; ; (equal (/ 3 2) 3/2) ; ; которое ACL2 примет после нажатия ENTER ; (аргументы equal должны быть равными). ; Заполняемое Вами значение должно быть атомом (который надо записать другим способом, ; если левая часть равенства уже атом). (equal (booleanp t) #) (equal (booleanp nil) #) (equal (booleanp 7) #) (equal (symbolp t) #) (equal (symbolp nil) #) (equal (atom t) #) (equal (consp nil) #) (equal (equal nil nil) #) (equal (equal nil t) #) (equal (equal T t) #) (equal (+ 5) #) (equal (+ 3 2 1) #) (equal (* -2) #) (equal (* 1 2 3) #) (equal (+) #) (equal (*) #) (equal (- 5) #) (equal (- -10) #) (equal (- 0) #) (equal (/ 1) #) (equal (/ 5) #) (equal (/ -2/3) #) (equal (equal 7/9 14/18) #) (equal (equal 8/2 4) #) (equal (* (- (+ 6 12) 1) 2) #) (equal -2/8 #) (equal (* 5 1/3) #) ; Числа - предикаты (возвращают значение t или nil) (equal (integerp -1) #) (equal (integerp 3/2) #) (equal (natp 1) #) (equal (natp 6/2) #) (equal (zp nil) #) (equal (zp 0000) #) (equal (posp 0) #) (equal (posp 4/2) #) (equal (integerp (first (rest (list -12 "b" "a" 0 43)))) #) ; Логические значения и/или функции (equal (not 0) #) (equal (and t (not nil) 13 (zp -1) 1/7) #) (equal (or (not 4) (natp -1) 0 1/7 (not t)) #) ; Списки: конструкторы и деструкторы (equal (first (cons 2 (cons 1 nil))) #) (equal (first (rest (cons 3 (list 2 1)))) #) (equal (rest (list nil)) #) (equal (rest (cons nil nil)) #) (equal (rest nil)) #) (equal (first 123) #) ; TrueLists: предикаты (equal (true-listp (cons (list 1 2) nil)) #) (equal (true-listp 11) #) (equal (endp "qqq") #) (equal (endp -0) #) (equal (consp (list 12)) #) (equal (consp (list) #)) ; Литералы (equal (equal '1 ''1) #) (equal (equal "ok" '"ok") #) (equal (equal -3 '-3) #) (equal (equal bb 'bb) #) ;is this a static error? if yes comment it out (equal (equal (f 3) '(f 3)) #) ;is this a static error? yes comment it out (equal (equal 'a ''a) #) (equal (equal (list 1 2 3) '(1 2 3)) #) (equal (equal (list 'a 'b) '(a b)) #) (equal (equal '(1 2 3) (quote (1 2 3))) #) (equal (car (car '('(1 2) '(3) '(4 5 6)))) #) (equal (car (car '((1 2) (3) (4 5 6)))) #) (defun foo (x) (list x 'x)) (equal (foo 3) #) ;; Часть 2: Рекурсивные определения ; Требуется представить определения функций для спецификаций, представленных ниже. ; Если нужно, можно использовать дополнительные определения функций. ; number-elements: true-list -> NumberedList ; NumberedList - это список, состоящий из 2-элементных списков. ; Рекомендация: определите вспомогательную рекурсивную функцию, ; у которой второй параметр - индекс. (defun number-elements (l) "Usage: Here is an example of how this works. Given the list (a b c) number-elements should return ((0 a) (1 b) (2 c)). In general, given a list l, number-elements numbers the elements of l by returning a 2-element list whose first element is the index, say n, and whose second element is the nth element of l. Indexing starts from 0." #) ; in: All true-list -> Boolean (defun in (x l) "Usage: Searches l for x and returns t if it is found, nil otherwise. " #) ; rem-dups: true-list -> true-list (defun rem-dups (l) "Usage: Returns a new list which is l without the duplicate elements" #) ; ordered-elementp: true-list -> Boolean (defun ordered-elementp (l) "Usage: Returns true if x is ordered with the relation <, nil otherwise." #) ; merge-ordered: OrderedList OrderedList -> OrderedList ; OrderedList is a list of elements ordered with the relation < (defun merge-ordered (l1 l2) "Usage: Returns a list containing the elements in l1 l2, ordered with the relation <" #)