Institute of Computer Science
  1. Courses
  2. 2022/23 fall
  3. Functional Programming (LTAT.03.019)
ET
Log in

Functional Programming 2022/23 fall

  • Üldinfo
    • Õppekorraldus
  • Loeng
    • Baasväärtused ja tüübid
    • 𝜆-arvutus
    • Kõrgemat järku funktsioonid
    • Interaktiivne programmeerimine
    • Uute tüüpide loomine
    • Liidesed
    • Sisend-Väljund
    • Laiskus
    • Lihtsalt tüübitud 𝜆-arvutus
    • Sõltuvad tüübid
    • Tõestamine Idrises
    • Kvantitatiivne tüübiteooria
  • Praktikum
    • KKK
    • Installimine
    • Kodutöö 1
    • Kodutöö 2
    • Kodutöö 3
    • Kodutöö 4
    • Kodutöö 5
    • Kodutöö 6
    • Kodutöö 7
    • Kodutöö 8
    • Kodutöö 9
    • Kodutöö 10
    • Kodutöö 11
    • Kodutöö 12
    • Kordamine
    • Projektid
  • Moodle
  • Zulip (sisselogides näed linki)

Lihtsalt tüübitud {$\lambda$}-arvutus

Tüübid spetsifitseerivad programmide omadusi.

  • {$\lambda$}-arvutuses klassifitseerivad normaalkujusid.
  • Kui term on tüüpi {$\text{Nat}$}, ja ta on normaalkujul, siis see term esitab naturaalarvu.

Tüübisüsteem koosneb kolmest komponendist:

  • tüüpide hulk;
  • programmide hulk;
  • tüüpimisreeglid.

Olgu antud loenduv hulk tüübimuutujaid (baastüübid). (Lihtsad tüübid = ei ole polümorfsed.)

Lihtsate tüüpide süntaks

{$ \begin{array}{lcl@{\hspace{5em}}l} \tau & ::= & \alpha & \mbox{tüübimuutuja} \\ & \mid & \tau_1 \to \tau_2 & \mbox{funktsioonitüüp} \end{array} $}

Tüübikonstruktor {${\to}$} on paremassotsiatiivne. {$ \tau_1 \to \tau_2 \to \tau_3 \equiv \tau_1 \to (\tau_2 \to \tau_3) $}

Church vs. Curry

Tüüpidega {$\lambda$}-avaldiste esitamiseks on kaks peamist stiili.

  • Church'i stiil: funktsiooni parameetrite tüübid esitatakse ilmutatult {$\lambda$}-termis {$\lambda x : \lambda.\ e$}.
    • Näiteks: {$\lambda x : \text{Nat}.\ x + x : \text{Nat} \to \text{Nat}$}.
    • Igal termil on unikaalne tüüp.
  • Curry stiil: termid on tavalised (s.o. ilma tüüpideta) ja kasutatakse tüübikorrektsuse predikaati (tüübituletus).
    • Näide: {$\lambda x.\ x + x : \text{Nat} \to \text{Nat}$}.
    • Termidel on palju tüüpe (näit. {$\lambda x.\ x : \text{Nat} \to \text{Nat}$}, kuid ka {$\lambda x.\ x : \text{Bool} \to \text{Bool}$}).

Meie kasutame põhiliselt esimest stiili.

Termid ja redutseerimine

Termide süntaks:

{$ \begin{array}{lcl@{\hspace{5em}}l} e & ::= & x & \mbox{muutuja} \\ & \mid & e_1\,e_2 & \mbox{aplikatsioon} \\ & \mid & \lambda x : \tau.\, e & \mbox{abstraktsioon} \end{array} $}

Samad süntaktilised konventsioonid kui puhtas {$\lambda$}-arvutuses.

Substitutsioon, reduktsioon jmt on defineertud analoogselt puhta $\lambda$-avutusega ignoreerides tüübiannotatsioone.

Tüüpimisrelatsioon

Et teha kindlaks mis termid on millist tüüpi, defineerime tüüpimisrelatsiooni.

Baasrelatsioon on kujul {$\Gamma \vdash e : \tau$}

  • term {$e$} on tüüpi {$\tau$} kontekstis {$\Gamma$}.

Kontekst {$\Gamma$} on muutujast ja tüübist koosnevate paaride jada {$\Gamma = \{x_1:\tau_1,\ \ldots,\ x_n:\tau_n\}$}.

  • Konteksti {$\Gamma$} doomenit tähistame

{$\text{dom}(\Gamma) = \{x_1,\ \ldots,\ x_n\}$}.

  • Korrektses tüüpimisrelatsioonis peab olema {$\text{fv}{e} \subseteq \text{dom}(\Gamma)$}.

{$\Gamma \leq \Delta$} tähendab, et kui {$x \in \text{dom}(\Gamma)$}, siis {$x \in \text{dom}(\Delta)$} ja {$\Gamma(x) = \Delta(x)$}.

Programm (s.o.\ kinnine term) {$e$} on tüüpi {$\tau$}, kui tal on see tüüp tühjas kontekstis: {$\vdash e : \tau$}.

Tüüpimisrelatsioon

Tüüpimisrelatsioon on defineeritud tüüpimisreeglite abil.

Lihtsalt tüübitud {$\lambda$}-arvutuse tüüpimisreeglid:

{$ \begin{array}{c} \hline
\Gamma, x:\tau \vdash x : \tau \end{array} $}

{$ \begin{array}{c} \Gamma, x:\sigma \vdash e : \tau\\ \hline
\Gamma \vdash \lambda x : \sigma.\,e : \sigma \to \tau \end{array} $}

{$ \begin{array}{c} \Gamma \vdash e_1 : \sigma \to \tau \quad \Gamma \vdash e_2 : \sigma\\ \hline
\Gamma \vdash e_1\,e_2 : \tau \end{array} $}

kus {$x \not\in\text{dom}(\Gamma)$}.

Edaspidi tähistame lihtsalt tüübitud {$\lambda$}-arvutust {$\lambda{\to}$}.

Tüübiohutus

Korrektselt tüübitud programmid ei lähe valesti.

Hind:

  • Mõned mõistlikud programmid hüljatakse.

Koosneb kahest osast:

  • Progress: Korrektselt tüübitud ei ole tupikus (ta on kas vöörtus või saab teha ühe väärtustusreeglitele vastava sammu).
  • Säilitamine: Kui korrektselt tüübitud term teeb ühe sammu, siis ka resultaat on korrektselt tüübitud.

Tüüpide unikaalsus, säilimine ja progress

Tüüpide unikaalsus: Kui {$\Gamma \vdash e : \tau_1$} ja {$\Gamma \vdash e : \tau_2$}, siis {$\tau_1 = \tau_2$}.

NB! Tüüpide unikaalsus ei kehti mitmete rikkamate keelte korral.

Tüüpide säilimine (subjekt-reduktsioon): Kui {$\Gamma \vdash e : \tau$} ja {$e \twoheadrightarrow e'$}, siis {$\Gamma \vdash e' : \tau$}.

Progress: Kui {$\Gamma \vdash e : \sigma$}, siis {$\exists e' : \sigma. e \rightarrow_\beta e'$} või {$e \in \mathrm{Val}$}, kus {$ v \in \mathrm{Val}\ ::=\ x\,v\,\ldots\,v \mid \lambda x{:}\tau.v $}

Tugev normaliseerimine: Lihtsalt tüübitud $\lambda$-arvutuses {$\lambda{\to}$} on iga {$\beta$}-reduktsiooni jada lõplik.

Mõned lihtsad järeldused:

  • Termide võrdsuse küsimus on lahenduv.
  • Püsipunktikombinaatorid ei ole defineeritavad.
  • Institute of Computer Science
  • Faculty of Science and Technology
  • University of Tartu
In case of technical problems or questions write to:

Contact the course organizers with the organizational and course content questions.
The proprietary copyrights of educational materials belong to the University of Tartu. The use of educational materials is permitted for the purposes and under the conditions provided for in the copyright law for the free use of a work. When using educational materials, the user is obligated to give credit to the author of the educational materials.
The use of educational materials for other purposes is allowed only with the prior written consent of the University of Tartu.
Terms of use for the Courses environment