038 — The Curry-Howard-Lambek Correspondence


#21

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:


#22

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.


#23

Ok, m-am mai gandit si cred ca exemplul tau este corect, dar exista produsul a x b si este a (vezi desen). Dar intr-adevar, nu exista produsul a x c. Probabil ca produsul nu paote fi defnit in termeni mai simplii decat el insusi (cum ar fi obiect terminal sau initial), ci in altii mai complexi (de exemplu, limita categoriei 2).

Edit: Daca nu gresesc, semnificatia produsului a x b in aceasta categorie este "cel mai mare element diin categorie care este mai mic sau egal cu a si mai mic sau egal cu b", deci daca exista a -> b, atunci produsul este a.

EditEdit: In aceasta categorie, a si c nu sunt comparabile. Defapt, exista “cel mai mare” element: b, dar nu exista cel mai mic. In exemplul tau, daca am avea un obiect initial, am avea si produs.

Dar in general, nu este suficient sa ai nici obiect initial, pentru ca ar putea exista mai multi candidati incomparabili (e si f) vezi imaginea de mai jos pentru un contra-exemplu construit peste categoria ta pentru “nu este suficient sa ai obiect terminal si obiect initial”:


#24

Corect. Am scris prost în postarea inițială. La inexistența a x c mă refeream (de-aia am și dat justificarea în postarea a doua cu rombul închis jos, deci ceva sub a și c). Mulțumesc de clarificare!

Cît despre definiția produsului în raport cu obiecte mai complexe sau mai simple, asta sună destul de meta (în sensul discuției despre ce-i mai simplu), dar am prins ideea. Nu am un răspuns sau alt comentariu, însă.


#25

Exact. Dar nu am avea sumă, dacă iei diagrama rotită cu 180 grade, adică un “V”, fără majorant comun. Asta dacă consideri situația simetrică, adică: doar cu obiect inițial, NU și terminal.

Edit: Desigur, e un truc clasic la mijloc: dualitatea categorială. Întorci săgețile și proprietățile și ai același tip de rezultat.