Tentamen i Specifikation och Härledning av Program

En postscript-version av samma dokument (utan de fel som programmet latex2html har infört) finns här.

Tentamen i kursen Specifikation och härledning av program (INN310) äger rum den 29:e Maj 1998, kl 8.45 - 13.45 i sal VÖ. Kursen ges av institutionen för Datavetenskap vid Göteborgs universitet. Inga hjälpmedel är tillåtna. Skriv bara på en sida av papperet! Lösningar till uppgifterna kommer att finnas på kursens hemsida. (www.cs.chalmers.se/-bengt/course/spec.html ). Tentamensvisning sker fredagen den 5:e juni kl 11.15 i S4.

1.
Ge ett bevisobjekt för $(X \in \mbox{\sf Set})(x \in X)\mbox{\sf Id}(X, x, x)$.
Svar: $[X][x]\mbox{\sf refl}(X,x,x)$ är ett sådant.

2 p.

2.
Låt A vara en mängd och P ett predikat över mängden. Man kan då ge P typen $(A)\mbox{\sf Set}$ eller $(A)\mbox{\sf Bool}$. Förklara skillnaden mellan dessa och ge ett exempel på ett predikat som har endast en av dessa typer.

Svar: I det första fallet är P en påstående-funktion, och det krävs alltså ett bevis för att visa att P är sann för ett visst värde. I det andra fallet är P en boolsk funktion som evaluerar till ett boolskt värde. I det fallet måste alltså P vara ett avgörbart predikat. Så om P är ett oavgörbart predikat, t.ex. predikatet som uttrycker att en heltals-funktion är lika med för varje argument, så har vi ett predikat som har den första typen men inte den andra.

3 p.

3.
Ge ett program som är ett bevisobjekt för $ (\neg A \mbox{$\,\vee\,$}\neg B) \supset\neg(A \,\&\,B) $.

Svar: Här är ett program F skrivet i något funktionellt språk:
\begin{align*}
F &= \supset_I\!\! (H)\\ H(\vee_{I1}\! (nota), \&_I\!(a,b)) &= nota(a)\\ H(\vee_{I2}\!(notb), \&_I\!(a,b)) & = notb(b)\end{align*}

3 p.

4.
Mängden $\Pi x \! \in \! A. B$ är en generalisering av funktionsmängden $A
\rightarrow B$. På vilket sätt? Varför kallas $\Pi x \! \in \! A. B$ för en kartesisk produkt över en familj av mängder?

Svar: I mängden $\Pi x \! \in \! A. B$ kan B bero på variabeln x. En funktion f i mängden $A
\rightarrow B$ är också ett element i mängden $\Pi x \! \in \! A. B$, men en funktion g i $\Pi x \! \in \! A. B$ är i allmänhet inte ett element i $A
\rightarrow B$. Typen av en applikation g(a) är B[x:=a], dvs beror i allmänhet av värdet av argumentet a.

Typen $\Pi x \! \in \! A. B$ kallas en kartesisk produkt eftersom om mängden A är t.ex. mängden $\{1,\ldots, 300\}$ kan man se ett element f i $\Pi x \! \in \! A. B$ som en tuppel i $B_{1}{\times}\ldots {\times}B_{300}$.

4 p.

5.
Vad är det för skillnad mellan $\Pi x \! \in \! A. B$ och $(x \in A)B$? Ge exempel där det ena kan användas men inte det andra samt vice versa.

Svar: Den första tar en mängd A och en familj av mängder B till en mängd. Den andra tar en typ A och en familj av typer B till en typ. Den första kan alltså användas i sammanhang där man förväntar sig en mängd, t.ex. $\Pi x \! \in \! A. B + \Sigma x \! \in \! A. B $. Den andra kan å andra sidan uttrycka kvantifiering över större saker än mängder, t.ex. $(x \in \mbox{\sf Set})x + x$, där + är disjunkt union.

8 p.

6.
Påståendet P(y) följer från påståendet P(x) om elementen x och y är påståendemässigt lika. Ge ett objekt i följande typ:

\begin{displaymath}
(A \in \mbox{\sf Set})(P \in (A)\mbox{\sf Set})(x,y \in A; \mbox{\sf Id}(A,x,y);P(x))P(y)\end{displaymath}

Använd eliminationsregeln för $\mbox{\sf Id}$-mängden.

Svar: Antag att $A \in \mbox{\sf Set}$, $ P \in (A)\mbox{\sf Set}$, $ a \in A$,$ b \in A$, $c \in \mbox{\sf Id}(A,a,b)$, $ d \in P(a)$. Vi vill hitta ett element i P(b). Eliminationsregeln för $\mbox{\sf Id}$-mängden

\begin{displaymath}
\begin{split}
\mbox{\sf idpeel}\in &(A \in \mbox{\sf Set};
C...
 ...\! (x \! \in \! A)C(x,x,\mbox{\sf refl}(x)))C(p,a,b)\end{split}\end{displaymath}

säger bl a att vi kan visa D(a,b) från $\mbox{\sf Id}(A,a,b)$ och $(x \! \in \! A)D(x,x)$. Iden är nu att låta $D(x,y) = P(x) \supset P(y)$, eftersom vi i så fall kan återföra problemet $P(a) \supset P(b)$ till det enkla problemet $ (x \! \in \! A)P(x) \supset P(x) $, som ju löses av $[x]\lambda([y]y)$.

Vi får alltså att

\begin{displaymath}
\mbox{\sf idpeel}(A, [x,y,u]P(x) \supset P(y),
a,b,c, [x]\lambda([y]y)) \in P(a) \supset P(b)\end{displaymath}

Återstår nu bara att använda modus ponens på detta och beviset av P(a):

\begin{displaymath}
\mbox{\sf apply}(\mbox{\sf idpeel}(A, [x,y,u]P(x) \supset P(y),
a,b,c, [x]\lambda([y]y)), d) \in P(b)\end{displaymath}

Det eftersökta objektet blir alltså:

\begin{displaymath}
\begin{split}[A,P,a,b,c,d]
\mbox{\sf apply}(\mbox{\sf idpeel}(\ldots, 
 \ldots, a,b,c, [x]\lambda([y]y)), d)\end{split}\end{displaymath}

10 p.

7.
Ge en formell beskrivning (bildnings-, introduktions-, eliminations- och likhets-regler) av följande mängdbildande operationer. Det är inte nödvändigt att ge triviala likhetsregler (regler som säger att något är lika om dess delar är lika).
(a)
$A {\times}B$, den kartesiska produkten mellan mängderna A och B.

Svar: Den kartesiska produkten kan beskrivas av följande definitioner:

\begin{displaymath}
\begin{align*}
 {\times}\ &\in (\mbox{\sf Set}, \mbox{\sf Se...
 ...\sf split}(A &,B,C,d,\mbox{\sf pair}(a,b)) = d(a,b)\end{align*}\end{displaymath}

2 p.

(b)
Mängden $A \! \leadsto \! \!B$ har element som är på en av följande tre former:
$\mbox{\sf nil}$
$\mbox{\sf atom}(b)$, där $b \in B$.
$\mbox{\sf fun}(c)$, där $c(x) \in A \! \leadsto \! \!B$ för $x \in A$.

Svar: Mängden $A \! \leadsto \! \!B$ kan beskrivas med hjälp av följande definitioner:

\begin{displaymath}
\begin{align*}
\! \leadsto \! \!&\in (\mbox{\sf Set};\mbox{\...
 ...f fun}(g)) = f(g,[x]\mbox{\sf treerec}(d,e,f,g(x)))\end{align*}\end{displaymath}

Lägg märke till hur man kan utnyttja induktionsantaganden $ (x \! \in \! A)C(c(x))$ vid beviset av $C(\mbox{\sf fun}(c))$.

12 p.
8.
Ge en formell beskrivning av en induktiv definition av B, mängden av binära heltal. En bra definition undviker inledande nollor samt saknar bevisobjekt i talen. Ge även en meningsfunktion $M \in
(B)\mbox{\sf N}$, som avbildar ett binärt heltal till dess mening som vanligt heltal.

Svar:

BB oneone MM Här är en definition (utan talet 0):

\begin{displaymath}
\begin{alignat*}
{2}
 \B & \in set \\ \one & \in B & \qquad ...
 ...1 & \in (B)B & \qquad M(1(x)) &= 2 * M(x) + 1 \\ \end{alignat*}\end{displaymath}

Man representerar alltså ett binärt tal genom att se siffrorna som postfixa konstruerare. Men det finns andra möjligheter...

16 p.

Lycka till!

Bengt Nordström (ank 1033)

About this document ...

This document was generated using the LaTeX2HTML translator Version 97.1 (release) (July 13th, 1997)


Bengt Nordstr|m
5/28/1998