BuK/IIm10/BuK-Kreativaufgabe10 G2

Wiki-Quelltext dieser Seite.

<language>Scheme</language>
<code id="4e0073febe720" hidden>
(define add1 (lambda (n)
    (+ n 1)))

(define sub1 (lambda (n)
    (- n 1)))

(define P (lambda (n)
    (if (= n 0)
        0
        (sub1 n))))
</code>

== Aufgabenstellung ==
Entwickeln Sie einen Werkzeugkasten  für primitiv rekursive Funktionen.
Es wird erwartet, dass aus primitiv rekursiven (Basis-)Funktionen unter Verwendung der
Kompositionstechniken (Substitution und primitive Rekursion) neue primitiv rekursive
Funktionen generiert werden. Diese sollen verwendbar sein.
Es wird nicht erwartet, dass ein universelles Beweisprogramm, das für eine gegebene
Funktion konstruktiv nachweist, dass sie primitiv rekursiv ist, entwickelt wird.

== Basisfunktionen ==
Zuerst definieren wir die Basisfunktionen.

<code id="4e007c5c98c1e">
(define S 
  (lambda (n)
    (add1 n)))

(define C0 
  (lambda n 0))

(define U 
  (lambda (i . n)
    (letrec
        ([helper
          (lambda (counter args)
            (if (= counter i)
                (car args)
                (helper (+ counter 1) (cdr args))))])
      (helper 1 n))))

(define U1 
  (lambda args
    (apply U (cons 1 args))))

(define U2
  (lambda args
    (apply U (cons 2 args))))
</code>

Die Nullfunktion kann mit beliebig vielen Parametern aufgerufen werden.
<run id="4e00745e40e2d">
(C0)
</run>
<run id="4e0076eb7301d">
(C0 1 2 3 4)
</run>

Die Projektionsfunktion erwartet als ersten Parameter den Inde des zu ermittelnden Arguments und anschließend eine variable Anzahl von Argumenten.
<run id="4e0076eb7309e">
(U 1 1 2 3)
</run>
<run id="4e0076eb73122">
(U 3 1 2 3)
</run>

Um spätere Beispiele einfacher zu gestalten, ist die Nutzung der konstanten Funktionen sinnvoll. 

<code>
(define C
  (lambda (q . n)
    (letrec
        ([helper
          (lambda (counter result)
            (if (= counter q)
                result
                (helper (+ counter 1) (S result))))])
      (helper 0 (C0 (U 1 n))))))
</code>

Als nächstes definieren wir die Substitution und die primitive Rekursion:
<code id="4e007c9ea7922">
(define my-apply
  (lambda (ls)
    (apply (car ls) (cdr ls))))

(define substitute
  (lambda (f . g)
    (lambda n
      (apply f
             (map my-apply
                  (map
                   (lambda (g_i)
                     (cons g_i n))
                   g))))))

(define prim-rec
  (lambda (f g)
    (lambda ni
      (letrec
          ([h
            (lambda (n1 rest)
              (if (= 0 n1)
                  (f rest)
                  (g n1 (h (P n1) rest) rest)
                  ))])
        (h (car ni) (cdr ni))))))
</code>

An Hand einiger Beispiele kann die Funktionsweise der beiden Prozeduren nachvollzogen werden.
Als erstes betrachten wir die Potenzierung. Die beiden benötigten 
Prozeduren <math>f</math> und <math>g</math> werden wie folgt definiert:

<code id="4e007c9ea79af">
(define pot-f
  (lambda (a)
    (C 1 a)))

(define pot-g
  (lambda (n h . args)
    (let ((x n) (a (caar args)))
      (mult (U 3 (P x) h a) 
            (U 2 (P x) h a)))))
</code>

Um nun aus diesen beiden Prozeduren die Potenzfunktion zu generieren wird die primitive Rekursion angewandt:

<code id="4e007c5c98dab">
(define pot-x-a (prim-rec pot-f pot-g))
</code>

<run id="4e007c5c99137">
(pot-x-a 2 5)
</run>

Möchte man lieber die Basis als erstes und die Potenz als zweites Argument übergeben, so kann durch Substitution eine Vertauschung der Parameter vorgenommen werden:
<code id="4e007c5c98e26">
(define pot (substitute pot-x-a 
                        (lambda x-y (apply U2 x-y))
                        (lambda x-y (apply U1 x-y))))
</code>

<run id="4e007c5c991c6">
(pot 5 2)
</run>

Ein weiteres Beispiel ist die Fakultätsfunktion:
<code id="4e007c5c98ebd">
(define fak-f
  (lambda args
    (C 1 args)))

(define fak-g
  (lamda (n h . args)
    (mult n h)))

(define fak (prim-rec fak-f fak-g))
</code>

<run id="4e007c5c99251">
(fak 5)
</run>

Monusfunktion:
<code id="4e007c5c98f3c">
(define monus-f
  (lambda (x)
    (apply U1 x)))

(define monus-g
  (lambda (n h . args)
    (P h)))

(define monus-y-x (prim-rec monus-f monus-g))
(define monus (substitute monus-y-x 
                          (lambda x-y (apply U2 x-y))
                          (lambda x-y (apply U1 x-y))))
</code>

<run id="4e007c5c99327">
(monus 1 3)
</run>
<run id="4e007c5c993d8">
(monus 3 3)
</run>
<run id="4e007c5c99487">
(monus 5 2)
</run>

Abstandsfunktion:
<code id="4e007c5c98fbb">
(define dist (substitute add monus monus-y-x))
</code>
<run id="4e007c5c9951c">
(dist 3 3)
</run>
<run id="4e007c5c995ae">
(dist 1 3)
</run>
<run id="4e007c5c9963f">
(dist 10 5)
</run>

Signumfunktion:
<code id="4e007c5c99054">
(define signum-f
  (lambda args
    (C 0 args)))

(define signum-g
  (lambda (n h . args)
    (C 1 args)))

(define signum (prim-rec signum-f signum-g))
</code>
<run id="4e007c5c996d3">
(signum 0)
</run>
<run id="4e007c5c99782">
(signum 3)
</run>