Λ-λογισμός με απλούς τύπους: Διαφορά μεταξύ των αναθεωρήσεων
Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
συ |
συνέχεια μετάφρασης |
||
Γραμμή 61:
: <math>o((\iota \to \iota) \to \iota) = 2</math>
== Σημασιολογία ==
=== Εγγενείς και εξωτερικές ερμηνείες ===
=== Θεωρία ισότητας ===
=== Λειτουργική σημασιολογία ===
=== Κατηγορική σημασιολογία ===
=== Σημασιολογία θεωρίας αποδείξεων ===
Ο λ-λογισμός με απλούς τύπους σχετίζεται πολύ με το επαγωγικό κομμάτι της προτασιακής [[ιντουισιονιστική λογική|ιντουισιονιστικής λογικής]] (δηλ. ελάχιστης λογικής) μέσω του ισομορφισμού Κάρυ-Χάουαρντ: οι όροι αντιστοιχούν ακριβώς σε αποδείξεις στην [[φυσική αναγωγή]], και οι μη-κενοί (ή ''κατοικημένοι'') τύποι είναι ταυτολογίες της ελάχιστης λογικής.
== Σημαντικά αποτελέσματα ==
| |||