038 — The Curry-Howard-Lambek Correspondence

Mulțumim,

Despre teoria categoriilor, în prezentare (din câte îmi amintesc) Denisa a menționat seria de articole “Category Theory for Programmers” de Bartosz Milewski.

Cartea (PDF) se află aici: https://github.com/hmemcpy/milewski-ctfp-pdf

Există și un Scala Edition.

Cartea asta cred că ar putea fi bună pt clubul de lectură.

1 Like

For whoever works better with an example, let me show you

(A & (B & C)) -> ((A & B) & C)
Spoiler alert, full solution inside

Logic

A & (B & C)          A & (B & C)
----------- (&e1)   ------------- (&e2)
     A                     B & C
                     --- (&e1)  --- (&e2)
                      B          C
------------------------ (&i)
          A & B
----------------------------------------- (&i)
                (A & B) & C

Type Theory

This becomes:

(a : A, (b : B, c : C)) -> ((a : A, b : B), c : C)

Which can be proved:

(a : A, (b : B, c : C))          (a : A, (b : B, c : C))
----------------------- (&e1)   ------------------------- (&e2)
     a : A                                 (b : B, c : C)
                                       ------ (&e1)   ------ (&e2)
                                        b : B          c : C
------------------------ (&i)
       (a : A, b : B)
-------------------------------------------------------------- (&i)
                      (a : A, b : B), c : C)

Same thing, in Haskell (called assoc, and given three types: A, B, and C):

assoc :: (A, (B,C)) -> ((A,B) -> C)
assoc (a, (b,c)) = ((a,b),c)

-- but we can make it generic as well, for any type:
assoc_ :: (a, (b, c)) -> ((a, b), c)
assoc_ (a, (b, c)) = ((a, b), c)

Category Theory

T is the terminal object, and t : T -> A x (B x C) is what we start with. We need to be able to obtain an arrow t' : T -> (A x B) x C).

By product A x (B x C), we know there exists p : A x (B x C) -> A and q : A x (B x C) -> B x C.

By composition, we can obtain the arrows p . t : T -> A and q . t : T -> B x C.

By product B x C, we know there exists p' : B x C -> B and q' : B x C -> C.

By composition, we can obtain the arrow p' . q . t : T -> B.

So now, we have the following arrows:

  • p . t : T -> A
  • p' . q . t : T -> B

By definition of product, since we know A x B is the product of A and B, and since we have the arrows T -> A and T -> B, then we know there must be an unique arrow which we’ll name l : T -> A x B.

By composition we can obtain the arrow q' . q . t : T -> C.

Similarly to the step before, by definition of product, since we know (A x B) x C is a product of A x B and C, and since we have the arrows l : T -> A x B and q' . q . t : T -> C, then there must exist an unique arrow t' : (A x B) x C.


An interesting observation is that you can easily see how they’re all doing the same thing. Let’s try writing the Haskell version without taking advantage of pattern matching:

assoc :: (a, (b, c)) -> ((a, b), c)
assoc a_bc = ((fst a_bc, fst (snd a_bc)), snd (snd a_bc))

-- or, we could do this:

intro :: a -> b -> (a, b)
intro a b = (a, b)

e1 :: (a, b) -> a
e1 = fst

e2 :: (a, b) -> b
e2 = snd

assoc :: (a, (b, c)) -> ((a, b), c)
assoc a_bc = intro (intro (e1 a_bc) (e1 (e2 a_bc)) (e2 (e2 a_bc))

If you follow the Logic proof from bottom to top, you’ll see that it:

  • ends with &i, which relates to our first (from the left) intro
    • its left side has an &i, which is the second intro in our code
      • this inner intro is composed from &e1 on the input, or premise, which is identical to what we write
      • the B is obtained by doing &e1 on &e2 on the premise, which is exactly what we do
    • its right hand side, C, is obtained by doing &e2 twice, which is identical to our code

If you follow the CT proof:

  • we could rewrite the l : T -> A x B arrow as <i,j> : T -> A x B, where i = p . t : T -> A and j = p' . q . t : T -> B.
  • we already have k = q' . q . t : T -> C

So let’s look closer at what i, j and k are:

  • i is p . t, which is the left projection of the premise, or fst a_bc

You may ask: Why?!? Well, p . t means p after t. In our case, t represents the input, so it’s equivalent to a_bc, and p is the left projection, which is equivalent to fst. Keep in mind that a . b . c means c first, then b, then a when reading the following.

  • j is p' . q . t, which is fst (snd a_bc)
  • l = <i,j>, so l = (fst a_bc, fst (snd a_bc))
  • k is snd (snd a_bc)
  • the result, T -> (A x B) x C is < <i,j>, k > = ((fst a_bc, fst (snd a_bc)), snd (snd a_bc))

If we look back at the Haskell definition:
assoc a_bc = ((fst a_bc, fst (snd a_bc)), snd (snd a_bc))


As for the other group, the first exercise is:

f :: forall a. a -> a -> a
Spoiler alert, full solution inside

There are only two implementations/proofs/inhabitants:

f1 :: forall a. a -> a -> a
f1 a _ = a

f2 :: forall a. a -> a -> a
f2 _ a = a

These two functions can be obtained through a different function that is a bit more useful:

ifThenElse :: Bool -> a -> a -> a
ifThenElse True a _ = a
ifThenElse False _ a = a

f1 :: a -> a -> a
f1 = ifThenElse True

f2 :: a -> a -> a
f2 = ifThenElse False

Not quite sure how to prove this though. It’s probably enough to uncurry and show that t1 :: T -> A and t2 :: T -> A are the only arrows from T to A.

Edit: added detailed explanation to the first Spoiler on how to see the equivalence between Logic and Haskell, and between Category Theory and Haskell.

1 Like

Mulțumim pentru materiale, excelente exerciții și exemple detaliate!

Schimb un pic direcția cu o întrebare: s-a menționat în tabelul de corespondențe între logică și teoria tipurilor legătura între logica modală și monade. Niște referințe pentru detalii se poate, vă rog?

Eu am găsit un articol și o prezentare destul de hardcore. :slight_smile:


Și o precizare din partea mea: O categorie cu un obiect terminal nu are neapărat produse binare. Este necesar să aibă pullbacks (exercițiu rezolvat și cazul particular pentru categoria Mon, a monoizilor).

Afirmația este, însă, adevărată pentru toposuri, la care aproape se ajunge în prezentarea Denisei, de îndată ce se introduc CCC.

Scuze pentru confuzie.

1 Like

Salut @adimanea!

In paper-ul lui Wadler exista o referire la Computational types from a logic perspective, unde am gasit:

Apoi cateva pagini mai jos:

Unde:

  • [Intro] ◇ a este return/pure
  • [Elim] ◇ a -> (a -> ◇ b) -> ◇ b este bind/>>=

Ideea este ca nu este precis definit, si poate diferi in functie de ce dorim sa facem:

  • poate reprezenta prezenta unei exceptii, caz in care ◇ a = a + 1 (altfel spus, Maybe a = Just a | Nothing)
  • poate reprezenta non-determinism, caz in care ◇ a = powerset(a) (altfel spus, [] a = [] | a : [a])
  • poate reprezenta citirea dintr-un mediu extern, caz in care ◇ a = env^a (altfel spus, Reader env a = env -> a (unde return = const si >>= este compozitie)

PS: In cautarile mele, am gasit si Modal Logic @Stanford unde apar cateva chestii interesante:

If A is a theorem of K, then so is ◻ A

Care arata exact a return / pure.

Distribution axiom: ◻ (A -> B) -> (◻ A -> ◻ B)

Care arata exact ca <*> :: f (a -> b) -> f a -> f b

Mai departe se mentioneaza de asemenea ca desi ar fi util in unele cazuri, nu se poate defini ◻ A -> A, ceea ce este adevarat si pentru monade (dar nu pentru co-monade).

Mersi mult pentru detalii și resurse!

Am cîteva elemente de logică modală însușite și astfel că prind bine exemplele de Haskell. Încă încerc să ies din interpretarea pur matematică. Despre monade începusem să citesc de la Moggi (în special ca să-mi scot [sau, mai bine zis, lărgesc] reflexul de a gîndi doar că o monadă este o algebră într-o categorie de functori), așa că, din nou, exemplele tale pică perfect!

Oarecum offtopic: recomand călduros și eu Stanford Encyclopedia of Philosophy! Acoperă cu mult mai mult decît filosofie, are paginile scrise de autori recunoscuți în domeniu, e actualizată periodic, are multe referințe; dau doar cîteva exemple la subiectul curent:

1 Like

Mulțumim pentru exerciții @cvlad! Am continuat exercițiul cu numărul de inhabitants al unui tip. Nu sunt sigur că e corect rezolvat, căci poate mi-au mai scăpat din implementări.

Spoiler
  • Pentru g :: forall a. a -> a -> a -> a, am găsit trei implementări:
g1 a1 a2 a3 = a1
g2 a1 a2 a3 = a2
g3 a1 a2 a3 = a3
  • Pentru h :: forall a b. (a -> b) -> a -> b, o singură implementare:
h = ($)
  • Pentru i :: forall a b c. (b -> c) -> (a -> b) -> a -> c, o singură implementare:
i = (.)
  • Pentru j :: forall a. a -> (), o singură implementare:
j = const ()
  • Pentru k :: forall a. a -> Bool, două implementări:
k1 = const True
k2 = const False
  • Pentru l :: Bool -> Bool, patru implementări:
l1 = const True
l2 = const False
l3 = id
l4 = not
  • Pentru m :: forall a. a -> [a], un număr infinit (?) de implementări:
m0 _ = []
m1 a = [a]
m2 a = [a, a]
...
m∞ a = [a, a, ...]

Pentru varianta categoric teoretică a primului exercițiu, nu mi-e întotdeauna clar cum ar trebui să intrepretez -> – ca un morfism în categorie sau ca un obiect exponențial?

@dan.oneata Yep, alea sunt rezolvarile care le aveam in cap cand am scris exercitiile. :+1: (Ti-am editat post-ul si am pus rezolvariile intr-un spoiler tag, in caz ca vrea si altcineva sa le rezolve).

Cat despre ->, acesta este intr-adevar un exponential in CT. In principiu, regula mea este urmatoarea:

  • daca am de demonstrat A -> B, atunci inseamna ca am un T -> A si trebuie sa ajung la T -> B, deci nu folosesc exponentiali aici
  • daca am A -> B -> C, ma folosesc de curry/uncurry si transform in: am T -> A si T -> B si trebuie sa ajung la T -> C
  • daca am (A -> B) -> A -> B, atunci nu cred ca se poate fara exponentiali, pentru ca trebuie sa avem ca premiza T -> (A -> B)
1 Like

@adimanea Pullback este f : X -> Z si g : Y -> Z, nu? Inteleg cum limita acestuia este produsul X * Y, dar ce nu inteleg este de ce nu este suficient sa luam limita categoriei 2 (care are doua elemente fara nicio sageata)?

Edit: Cred ca acelasi lucru pot spune despre coprodus, si anume ca ar fi colimita imaginii categoriei 2.

EditEdit: Defapt, cred ca limita oricarei discrete category este (n)-produsul, nu?

Salut @cvlad!

Ai cumva o referință care să explice de ce “limita pullback-ului este produsul” – sau am înțeles eu greșit? Întreb pentru că nu mi-e foarte clar ce înseamnă “limita unui pullback”, pentru că noțiunea de limită e, de obicei, definită pentru un functor.

Salut,

Eu ce am in cap (si poate fi total gresit) este asa:

  • pornim de la o categorie C
  • alegem categoria discreta 2
  • pentru orice functor F : 2 -> C (care practic ne va “alege” doua* obiecte din C)
  • pentru orice obiect x din C, avem un functor constant Const(x) : 2 -> C (e.g. daca avem un obiect A in C, atunci Const(A) ne da A)
  • avem un natural transform: alpha(x) : Const(x) -> F astfel incat diagramele comuta (conform regulilor de natural transform)
  • exista o sageata unica intre orice obiect Const(x) si lim(F), adica f(x) : Const(x) -> lim(F)

Atunci, pentru un F care “alege” obiectele 1 -> A si 2 -> B, atunci daca lim(F) = AxB (produsul) atunci alpha(AxB)(1) va fi fst si alpha(AxB)(2) va fi snd.

Cred ca daca luam toate variantele posibile de functor F, putem spune ca avem produs in categoria C. Altfel, daca luam o singura instanta, putem spune doar ca pentru F care duce 1 -> A si 2 -> B, atunci lim(F) va fi produsul A x B.

(*) Functorul F poate alege un singur element, si asta este cazul de produs A * A, care este ok si el.

Edit: Incurcasem sagetile pentru alpha(x); este Const(x) -> F.

Da, are sens – limita functorului F : 2C ne dă produsul lui F 1 și F 2.

Ce nu înțelesăsem eu era legătura cu pullback-urile. Dar bănuiesc că ideea e că dacă o categorie are pullback-uri, are automat și produse; confrom Wikipedia:

The pullback is similar to the product, but not the same. One may obtain the product by “forgetting” that the morphisms f and g exist, and forgetting that the object Z exists.

1 Like

Sigur nu poate funcționa chestia asta, fiindcă ar trebui să ai produse binare în orice categorie, ceea ce nu e adevărat (dar nici nu-s contraexemple “la îndemînă”). Bănuiala mea e că ultimele 2 bulinuțe din argumentarea ta nu țin mereu (transformarea naturală și limF).

Mai rumeg și revin, trebuie să revăd unde se folosește esențial pullback-ul și poate vin și cu un contraexemplu.

Repet, pentru categoriile “obișnuite” cred că merge, de-aia curge natural argumentul tău. Dar sigur există ceva spații topologice sau clase proprii (categorii mari) sau ceva ciudățenii unde nu merge. :slight_smile:

Revin cînd am ceva concret.

Edit: Transformările naturale, pullback-urile și chiar produsele nu-s tocmai “gratis”, chiar dacă în categorii de mulțimi sau structuri algebrice sînt clare. Asta e ideea principală pe baza căreia o să încerc să te contrazic. Cu ceva “categorii scheletice” (categorii de diagrame) sau virgulă (comma) sau cu poseturi, nu știu acum. Dar m-aștept să fie ceva subtil.

Edit2: Categoria 2 trebuie să aibă identități, totuși.

Categoria discretă nu e un exemplu de categorie fără produse? (Prin categorie discretă înțeleg o categorie care are ca morfisme doar morfismele identitate)

Da, corect. Ai dreptate.

Poate exprimarea mea ar trebui sa fie "daca exista acest natural transform alpha(x), atunci…? Pentru mine este de multe ori vag ce “ai voie” si ce “nu ai voie” sa faci intr-o categorie.

O construiesc cum vreau? Observ doar ce proprietati are prin alte categorii/functori pe care ii construiesc cum vreau? Depinde de context, si ce incerc sa demonstrez? :slight_smile:

Da, cred că e corect cu dacă… Apoi, privitor la “ce ai voie”, de multe ori ideea este să meargă construcția “naturală” (evidentă). Dacă nu merge aia, aproape sigur nu merge în general. Știu că e și mai vag ce zic aici, dar așa am văzut că merg lucrurile.

Alternativ, ca să elimini acest vag și “gut instinct”, definești cum vrei, dar efectiv trebuie să verifici toate axiomele. Pot cădea chestii la cel mai mic detaliu, de-aia trebuie verificate toate detaliile cu construcția ta. Iar cînd ai pretenția unei afirmații “pentru orice categorie”, acolo e extrem de riscant. Concret: există categorii în care epi nu e surjectiv (și mono nu e injectiv). Dar n-aș numi niciodată contraexemplele “naturale”. (Așa cum aș numi, însă, naturală așteptarea ca aceste contraexemple să nu existe.).

2 Likes

Revin, cu întîrziere, cu contraexemplul.

Fie categoria dată de poset-ul a < b, c < b, dar a și c incomparabile.

Atunci ai săgeată x -> y dacă și numai dacă x < y. Deci b este obiectul terminal.

Pe de altă parte, dacă ar fi să existe produsul lui a și b, el ar fi infimumul lor, elementul mai mic decît ambele (pentru că ar trebui să existe proiecțiile pe factori), cu proprietatea de universalitate din definiție.

Or așa ceva nu avem.

Deci e o categorie cu obiect terminal, dar fără produse.

Sper că nu mi-a scăpat ceva.

Daca sagetile sunt <, atunci identitatea are alta semnificatie/semantica? Are sens intrebarea? Cred ca am mai dat o data de problema asta si n-am avut pe cine sa intreb :slight_smile:

Edit: Si acum ca am incercat un pic sa diger si restul, pentru mine iar incepe sa fie complicat sa inteleg cand “am voie” sa adaug obiecte si sageti in categoria data ca exemplu.

Intuitia imi spune ca daca as avea un produs a x b, ar trebui sa fie ceva mai mic si decat a si decat b, dar cum am a < b, atunci este redundant si ar trebui sa fie izomorfic cu b, deci ar trebui sa am produs si aici… desi imi este greu momentan sa vad cum demonstrez. Ma mai gandesc. :slight_smile:

Săgețile nu pot fi ordinea strictă <, îmi cer scuze. Însuși numele de POset vine de la “partially ordered set”, iar o ordine parțială e obligatoriu reflexivă. Scuze pentru ambiguitate. <-ul meu e de fapt ≤.

Privitor la partea a doua a comentariului, înțeleg ce zici, dar chiar și izomorfismul (cu b), dacă ar fi să existe, pentru un alt obiect, el se definește prin “săgeată + epi + mono”, toate cele 3 fiind interpretate în sens de poset. Deci îl poți adăuga, cu un pic de atenție astfel încît să se satisfacă proprietățile. Dar, desigur, nu ar mai fi posetul nostru. Ai voie, dar obții altceva. Categoria dată are doar 2 săgeți (în afară de id).

Legat de “redundanța” de care zici, aici faci apel la tranzitivitate, de fapt. Dar e mai simplu de vizualizat, ăsta e avantajul poset-urilor. Desenezi și stabilești niște niveluri orizontale și verticale. Pe orizontală ai elementele incomparabile, pe verticală ai relația ≤. Ce vrei, de fapt, pentru existența produsului, în cazul de față, e să se închidă jos rombul cu cele 3 vîrfuri date. Nu poate fi tot b sau o copie izomorfă a lui acolo, pentru că în poset ar fi totuna.

În particular, monomorfismele sînt triviale. Să examinăm definiția: ’fg = fh => g = h’. Ipoteza înseamnă 2 drumuri concatenabile, alcătuite din cîte 2 porțiuni, dar una comună conduce la concluzia că și partea a doua e comună, deci drumurile coincid. Intuitiv, e clar că asta ține în orice poset și arată că izomorfismele sînt musai identități, nu există cópii (izomorfe, dar) neidentice.

Sper că am înțeles corect ce spuneai și ajută cele de mai sus.

Edit: Dacă ar fi să înțeleg mot-a-mot ce ai zis privitor la adăugarea de obiecte și săgeți, răspunsul e că niciodată nu ai voie să pui unele noi fără a schimba categoria. Categoria dată (în particular, asta simplă dată de mine) are fix obiectele și săgețile din definiție. Iar atunci e simplu de rezolvat orice problemă care conține “există un obiect/o săgeată astfel încît”, prin epuizarea cazurilor, fiindcă doar ce a fost dat de la început există.

Probabil tu te gîndeai mai mult la cazurile “serioase”, eventual infinite, unde demonstrația existenței poate fi constructivă, deci pare că adaugi obiecte sau săgeți. Dar aici nu e cazul.