Kihagyás

1. előadás

Követelmények

  • Kezdés: 16:00
  • Nincs előadás felvétel
  • teaching / tipuselmelet
    • bitbucket.org/akaposi/ttt
  • Katalógus
    • GDPR issues
    • Visual proof
    • Totally spies?? amogus
  • Canvas kvízek
    • Előző előadásig bezárólag
    • Pontok: \(\text{canvas\_kviz}() \rightarrow {0; 1}\)
    • Vizsga előkövetelmény: 50%
    • Egyszer lehet kitölteni
  • Gyakorlati +/-
    • Gyakorlat előkövetelmény: 50%

Gyakorlat ponthatárok

pontszám jegy
0 - 4.999 1
5 - 6.249 2
6.25 - 7.49 3
7.5 - 8.749 4
8.75 - 5

Per Martin-Löf's type theory

  • Curry-Howard izomorfizmus
  • Kategória
  • ZFC
  • Mi az a függvény?
Agda Típuselmélet
Haskell System F (polimorf lambda kalkulus)
Lisp Lambda kalkulus (Turing gép)

Típuselméletre épül

  • Agda
    • Svéd
    • Legtöbb szolgáltatás
    • Szintaxisa hasonlít a haskellhez
  • Lean
    • Amerikai
    • Matematikai (klasszikus bizonyítás)
  • Coq
    • Fr*nch
    • Most advanced, apparently
    • Used in Chromium's SSL impl??
  • Idris
    • Sköt
    • Programing oriented
    • Cringe

Basically, constrictive means that you have your first constant, and a function to generate each item in your universe

Matematika: elsőrendű logika + halmazelmélet axiómák OR típuselmélet

add2' : Nat -> Nat
add2' x = x + 2 

add2 : Nat -> Nat
add2 = \ x -> x + 2

\(\Beta\) redukció

add2 3 = (def) ($\lambda$ x \tightarrow x + 2) (\(\Beta\) redukció ) (x + 2) [x $\rightarrow$ 3] = 3 + 2 = 5

plus : Nat -> Nat -> Nat
plus x y = x + y

Magasabb rendű

k: (Nat -> Nat) -> Nat
k h = h4 + h 3