=====Protokoll SemProg 29.7.2013=====

Prüfer: Daniel Gorín, Lutz Schröder

====Fragen====

==Was macht »omega«?===

  löst pressburger-arithmetik


==Wie ist in coq der existenzquantor definiert?==

antwort wäre gewesen:
  Inductive ex (X:Type) (P : X->Prop) : Prop :=
    ex_intro : forall (witness:X), P witness -> ex X P.

hab mich bissi vertan, und
  Inductive ex {X : Type} (x : X) ...

angefangen, so dass wir einen kleinen ausflug nach "welchen typ hat der ausdruck »X > 5«? (nat -> Prop) gemacht haben.

==Was ist denn die »functional extensionality«?==

Axiom, das sagt, dass wenn forall x. f x = g x, dann ist f = g. ist in coq so nicht beweisbar, weil nur dinge für die man einen beweis konstruieren kann beweisbar sind.


==Wir ham da mal so n programm, was sagst du so dazu==

  Axiom funny: exists (X Y : Type) (x : X) (f g : X -> Y), f x = g x -> f = g.

also functional extensionality, nur mit existenz- statt allquantor.

==Was sind denn diese hoare-tripel?==

tripel aus vorbedingung, codestück und nachbedingung. wenns gültig ist, dann sagts, dass falls vorbedingung gilt, und codestück terminiert, dannach nachbedingung gilt.

==schreib doch mal eine der hoare-regeln hin==

  (hoare_asgn) ---------------------------
                {{[X/s]P}} X := s {{P}}

==wenn man jetzt eine hoare-regel für eine for-schleife wie in C-ähnlichen sprachen haben wollen würde..==

for-schleife allgemein
  FOR (C1; guard; C2) { C3 }

hoare-tripel
  {{P'}}C1{{P}}     {{P}} WHILE guard DO C3; C2 END {{P ∧ ¬guard}}
  ----------------------------------------------------------------
    {{P'}} FOR (C1; guard; C2) { C3 } {{P ∧ ¬guard}}


===Ergebnis===
damit war die zeit auch schon rum, leider (auch etwas zu daniels überraschung), und die ganzen coolen dinge, wie typ-foo (progress, typerhaltung) und lambda-zeugs kamen garned dran :-/

zusammen mit meinem übungsabgabenergebnis von umgerechnet 2.4 wars am ende ne 2.0