From c5fcf7179a83ef65c86c6a4a390029149e518649 Mon Sep 17 00:00:00 2001 From: Franciszek Malinka Date: Tue, 5 Oct 2021 21:49:54 +0200 Subject: Duzy commit ze smieciami --- Semestr 2/racket/egzamin/zad2.rkt | 186 -------------------------------------- 1 file changed, 186 deletions(-) delete mode 100644 Semestr 2/racket/egzamin/zad2.rkt (limited to 'Semestr 2/racket/egzamin/zad2.rkt') diff --git a/Semestr 2/racket/egzamin/zad2.rkt b/Semestr 2/racket/egzamin/zad2.rkt deleted file mode 100644 index e549f07..0000000 --- a/Semestr 2/racket/egzamin/zad2.rkt +++ /dev/null @@ -1,186 +0,0 @@ -#lang racket - -;; Oświadczam, że rozwiązanie zadania egzaminacyjnego przygotowałem -;; w pełni samodzielnie, korzystając wyłącznie z materiałów do wykładu, -;; notatek, podręcznika, oraz materiałów zacytowanych w treści rozwiązania. -;; Oświadczam że nie korzystałem w żadnej formie z pomocy osób trzecich -;; w przygotowaniu rozwiązania ani też takiej pomocy nie udzielałem -;; i nie udostępniałem nikomu swojego rozwiązania. - -;; ZADANIE 2 -;; ========= - -;; W tym zadaniu przyjrzymy się pierwszemu "językowi programowania" -;; który widzieliśmy na zajęciach: wyrażeniom arytmetycznym. Ich -;; prostota przejawia się przede wszystkim tym że nie występują w nich -;; zmienne (a w szczególności ich wiązanie) — dlatego możemy o nich -;; wnioskować nie używając narzędzi cięższych niż te poznane na -;; wykładzie. - -;; W tym zadaniu będziemy chcieli udowodnić że nasza prosta kompilacja -;; do odwrotnej notacji polskiej jest poprawna. Konkretniej, należy -;; · sformułować zasady indukcji dla obydwu typów danych -;; reprezentujących wyrażenia (expr? i rpn-expr?) -;; · sformułować i udowodnić twierdzenie mówiące że kompilacja -;; zachowuje wartość programu, tj. że obliczenie wartości programu -;; jest równoważne skompilowaniu go do RPN i obliczeniu. -;; · sformułować i udowodnić twierdzenie mówiące że translacja z RPN -;; do wyrażeń arytmetycznych (ta która była zadaniem domowym; -;; implementacja jest poniżej) jest (prawą) odwrotnością translacji -;; do RPN (czyli że jak zaczniemy od wyrażenia i przetłumaczymy do -;; RPN i z powrotem, to dostaniemy to samo wyrażenie). -;; Swoje rozwiązanie należy wpisać na końcu tego szablonu w -;; komentarzu, podobnie do niniejszej treści zadania; proszę zadbać o -;; czytelność dowodów! - -(struct const (val) #:transparent) -(struct binop (op l r) #:transparent) - -(define (operator? x) - (member x '(+ * - /))) - -(define (expr? e) - (match e - [(const v) - (integer? v)] - [(binop op l r) - (and (operator? op) - (expr? l) - (expr? r))] - [_ false])) - - -(define (value? v) - (number? v)) - -(define (op->proc op) - (match op - ['+ +] - ['- -] - ['* *] - ['/ /])) - -;; zał: (expr? e) jest prawdą -;; (value? (eval e)) jest prawdą -(define (eval e) - (match e - [(const v) v] - [(binop op l r) - (let ((vl (eval l)) - (vr (eval r)) - (p (op->proc op))) - (p vl vr))])) - -(define (rpn-expr? e) - (and (list? e) - (pair? e) - (andmap (lambda (x) (or (number? x) (operator? x))) e))) - -;; mój kod -(define (parse-expr q) - (cond - [(integer? q) (const q)] - [(and (list? q) (= (length q) 3) (operator? (first q))) - (binop (first q) (parse-expr (second q)) (parse-expr (third q)))])) - -(struct stack (xs)) - -(define empty-stack (stack null)) -(define (empty-stack? s) (null? (stack-xs s))) -(define (top s) (car (stack-xs s))) -(define (push a s) (stack (cons a (stack-xs s)))) -(define (pop s) (stack (cdr (stack-xs s)))) - - -(define (eval-am e s) - (cond - [(null? e) (top s)] - [(number? (car e)) (eval-am (cdr e) (push (car e) s))] - [(operator? (car e)) - (let* ((vr (top s)) - (s (pop s)) - (vl (top s)) - (s (pop s)) - (v ((op->proc (car e)) vl vr))) - (eval-am (cdr e) (push v s)))])) - -(define (rpn-eval e) - (eval-am e empty-stack)) - -(define (arith->rpn e) - (match e - [(const v) (list v)] - [(binop op l r) (append (arith->rpn l) (arith->rpn r) (list op))])) - -(define (rpn-translate e s) - (cond - [(null? e) - (top s)] - - [(number? (car e)) - (rpn-translate (cdr e) (push (const (car e)) s))] - - [(operator? (car e)) - (let* ((er (top s)) - (s (pop s)) - (el (top s)) - (s (pop s)) - (en (binop (car e) el er))) - (rpn-translate (cdr e) (push en s)))])) - -(define (rpn->arith e) - (rpn-translate e empty-stack)) - - -;; W kilku miejscach pozwoliłem sobie zapomnieć że symbol operatora i operator -;; to nie to samo, ale nie ma to znaczenia w kontekście dowodów. -;; Przez ES oznaczam empty-stack -;; -;; Zasada indukcji dla expr: -;; Dla dowolnej własności P, jeśli -;; · zachodzi P((const x)) dla dowolnego x oraz -;; · dla dowolnych e1, e2 oraz operator op jeśli zachodzi P(e1), P(e2) -;; to zachodzi P((binop op e1 e2)) -;; to dla dowolnego e, jeśli zachodzi (expr? e) to zachodzi P(e) -;; -;; Zasada indukcji dla rpn (ale tego wg rpn-expr?): -;; Dla dowolnej własności P, jeśli -;; · zachodzi P(x) dla dowolnej liczby lub opeartora x oraz -;; · dla dowolnej listy liczb lub operatorów xs oraz dowolnej liczby lub -;; operatora x, jesli zachodzi P(xs), to zachodzi P((cons x xs)) -;; to dla dowolnej listy xs liczb lub operatorów zachodzi P(xs) -;; -;; -;; Tw. 1: Jeśli spełnione jest (expr? e), to (eval e) ≡ (rpn-eval (arith->rpn e)) -;; -;; D-d. Skorzystamy z zasady indukcji dla wyrażeń. -;; · Weźmy dowolną liczbę x. Wtedy jeśli e ≡ (const x), to zachodzi -;; (eval (const x)) ≡ x ≡ (rpn-eval '(x)) ≡ (rpn-eval (arith->rpn (const x))) -;; · Weźmy dowolne e1, e2 spełniające naszą tezę oraz jakiś operator op. Wtedy -;; (eval (binop op e1 e2)) ≡ -;; (op (eval e1) (eval e2)) ≡ [Z definicji eval-am] -;; (eval-am '() (push (op (eval e1) (eval e2)) ES)) ≡ -;; (eval-am '(op) (push (eval e2) (push (eval e1) ES))) ≡ [Z założenia indukcyjnego] -;; (eval-am '(op) (push (rpn-eval (arith->rpn e2)) (push (eval e1) ES))) ≡ -;; (eval-am (append (arith->rpn e2) '(op)) (push (eval e1) ES)) ≡ [Z założenia indukcyjnego] -;; (eval-am (append (arith->rpn e1) (arith->rpn e2) '(op)) ES) ≡ -;; (rpn-eval (append (arith->rpn e1) (arith->rpn e2) '(op))) ≡ [Z definicji arith->rpn] -;; (rpn-eval (arith->rpn (binop op e1 e2))) -;; Pokazaliśmy oba warunki indukcji dla wyrażeń, zatem twierdzenie prawdziwe jest -;; dla dowolnego wyrażenia e spełniającego (expr? e). -;; -;; Tw. 2: Jeśli spełnione jest (expr? e), to (rpn->arith (arith->rpn e)) ≡ e -;; -;; D-d. Skoryzstamy z indukcji dla wyrażeń. -;; · Weźmy dowolną liczbę x. Wtedy dla e ≡ (const x) zachodzi -;; (rpn->arith (arith->rpn e)) ≡ (rpn->arith '(x)) ≡ (const x) -;; · Weźmy dowolne e1, e2 dla których twierdzenie zachodzi oraz operator op. Wtedy -;; (rpn->arith (arith->rpn (binop op e1 e2))) ≡ [Z definicji arith->rpn] -;; (rpn->arith (append (arith->rpn e1) (arith->rpn e2) '(op))) ≡ -;; (rpn-translate (append (arith->rpn e1) (arith->rpn e2) '(op)) ES) ≡ [Z zał. (arith->rpn e1) ewaluuje się do liczby] -;; (rpn-translate (append (arith->rpn e2) '(op)) (push e1 ES)) ≡ [Z zał. (arith->rpn e2) ewaluuje się do liczby] -;; (rpn-translate '(op) (push e2 (push e1 ES))) ≡ [Z definicji rpn-translate] -;; (rpn-translate '() (push (binop op e1 e2) ES)) ≡ -;; (binop op e1 e2) -;; Pokazaliśmy oba warunki indukcji dla wyrażeń, zatem twierdzenie jest prawdziwe -;; dla dowolnego e spełniającego (expr? e). -- cgit v1.2.3