Many-sorted logic (original) (raw)
Η λογική με πολλούς τύπους (many-sorted logic) μπορεί να αναπαριστά τυπικά την πρόθεση να μη χειριζόμαστε το σύμπαν σαν μια ομογενή συλλογή από αντικείμενα, αλλά να χωρίζεται αυτό με τρόπο παρόμοιο με αυτόν των τύπων του προγραμματισμού με τύπους. Τα συναρτησιακά και τα βεβαιωτικά (assertive) "μέρη του λόγου" της γλώσσας της λογικής ανακλούν αυτόν τον χωρισμό του σύμπαντος με τύπους, ακόμα και στο συντακτικό επίπεδο: η αντικατάσταση και το πέρασμα παραμέτρων μπορούν να γίνουν μόνο με αυτόν τον τρόπο, σεβόμενοι τους "τύπους".
| Property | Value |
|---|---|
| dbo:abstract | Sortenlogik entspringt der Intention, das (mengentheoretische) Universum (Grundmenge, Allklasse, bis hin zu einem Grothendieck-Universum) nicht als eine homogene Ansammlung von (mathematischen) Objekten zu betrachten, sondern diese auf verschiedene Klassen oder Typen aufzuteilen, die in diesem Zusammenhang Sorten genannt werden (ähnlich wie die Datentypen in vielen Programmiersprachen und Datenbanksystemen). Jedem Term einer logischen Formel wird eine Sorte zugeordnet. Unifikation von Termen ist nur dann zugelassen, wenn beide Terme von der gleichen Sorte sind; Substitution und Argumentübergabe können ebenfalls nur unter Berücksichtigung dieser Sorten erfolgen. Falsche Sortenzuordnungen werden also bereits als Syntaxfehler ausgewiesen.(Siehe auch: Objekt (Programmierung), mathematische Formel und Substitution (Mathematik)) (Siehe auch: Argumente und Funktionale Programmierung) (de) Η λογική με πολλούς τύπους (many-sorted logic) μπορεί να αναπαριστά τυπικά την πρόθεση να μη χειριζόμαστε το σύμπαν σαν μια ομογενή συλλογή από αντικείμενα, αλλά να χωρίζεται αυτό με τρόπο παρόμοιο με αυτόν των τύπων του προγραμματισμού με τύπους. Τα συναρτησιακά και τα βεβαιωτικά (assertive) "μέρη του λόγου" της γλώσσας της λογικής ανακλούν αυτόν τον χωρισμό του σύμπαντος με τύπους, ακόμα και στο συντακτικό επίπεδο: η αντικατάσταση και το πέρασμα παραμέτρων μπορούν να γίνουν μόνο με αυτόν τον τρόπο, σεβόμενοι τους "τύπους". Υπάρχουν πολλοί τρόποι για την τυποποίηση της παραπάνω πρόθεσης: μια λογική με πολλούς τύπους είναι κάθε "πακέτο" πληροφοριών που την ικανοποιεί. Στις περισσότερες περιπτώσεις δίνονται τα εξής: * ένα σύνολο από τύπους (sorts), S * μια κατάλληλη γενίκευση της έννοιας της υπογραφής (ή οπλισμού, αγγλ. signature) για να μπορεί να γίνει χειρισμός της επιπλέον πληροφορίας που έρχεται με τους τύπους. Το πεδίο τότε κάθε δομής αυτής της υπογραφής χωρίζεται σε διακριτά υποσύνολα, ένα για κάθε τύπο. (el) Many-sorted logic can reflect formally our intention not to handle the universe as a homogeneous collection of objects, but to partition it in a way that is similar to types in typeful programming. Both functional and assertive "parts of speech" in the language of the logic reflect this typeful partitioning of the universe, even on the syntax level: substitution and argument passing can be done only accordingly, respecting the "sorts". There are various ways to formalize the intention mentioned above; a many-sorted logic is any package of information which fulfils it. In most cases, the following are given: * a set of sorts, S * an appropriate generalization of the notion of signature to be able to handle the additional information that comes with the sorts. The domain of discourse of any structure of that signature is then fragmented into disjoint subsets, one for every sort. (en) A lógica polissortida pode refletir formalmente a nossa intenção de não lidar com o universo como um conjunto homogêneo de objetos, mas particionar isso de uma maneira que é semelhante aos de tipos em linguagens tipadas. Ambos funcionais e assertivas "partes do discurso" na linguagem da logica refletem essa partição tipificada do universo, mesmo no nível de sintaxe: substituição e argumento de passagem só pode ser feito em conformidade, respeitando os "tipos". Há mais maneiras de formalizar a intenção acima mencionada; a Lógica polissortida é qualquer pacote de informação que o preenche. Na maioria dos casos, são os seguintes dados: * um conjunto de tipos, S * uma generalização adequada da noção de assinatura ara ser capaz de lidar com a informação adicional que vem com os tipos. O universo de discurso de qualquer estrutura dessa assinatura é então fragmentada em subconjuntos dijuntos, um para cada tipo. (pt) |
| dbo:thumbnail | wiki-commons:Special:FilePath/Sort_hierarchy.png?width=300 |
| dbo:wikiPageExternalLink | https://web.archive.org/web/20070102043747/http:/react.cs.uni-sb.de/~zarba/ https://web.archive.org/web/20070608182648/http:/react.cs.uni-sb.de/~zarba/notes.html https://web.archive.org/web/20150220005037/http:/gdz.sub.uni-goettingen.de/index.php%3Fid=11&L=4&PPN=GDZPPN002289989&L=1%7C http://archive.numdam.org/article/CM_1956-1958__13__277_0.pdf https://www.sfu.ca/~jeffpell/papers/SortalRestrQuant.pdf%7C http://gdz.sub.uni-goettingen.de/index.php%3Fid=11&L=4&PPN=GDZPPN002289989&L=1%7C |
| dbo:wikiPageID | 8169758 (xsd:integer) |
| dbo:wikiPageLength | 8767 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1119199895 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Categorical_logic dbr:Homogeneous dbr:Christoph_Walther dbr:Lexical_category dbr:Parametric_polymorphism dbr:Structure_(mathematical_logic) dbr:Type_system dbr:Liskov_substitution_principle dbc:Systems_of_formal_logic dbr:Partition_(number_theory) dbr:Template_(C++) dbr:Abstract_algebraic_logic dbr:Domain_of_discourse dbr:Signature_(logic) dbr:Order-sorted_unification dbr:Many-sorted_first-order_logic dbr:Overloading_(programming) dbr:File:Sort_hierarchy.png |
| dbp:wikiPageUsesTemplate | dbt:Cite_journal dbt:Portal dbt:Reflist dbt:Short_description |
| dct:subject | dbc:Systems_of_formal_logic |
| rdf:type | yago:Ability105616246 yago:Abstraction100002137 yago:Cognition100023271 yago:Know-how105616786 yago:Logic105664069 yago:Method105660268 yago:PsychologicalFeature100023100 yago:System105661996 yago:WikicatSystemsOfFormalLogic |
| rdfs:comment | Η λογική με πολλούς τύπους (many-sorted logic) μπορεί να αναπαριστά τυπικά την πρόθεση να μη χειριζόμαστε το σύμπαν σαν μια ομογενή συλλογή από αντικείμενα, αλλά να χωρίζεται αυτό με τρόπο παρόμοιο με αυτόν των τύπων του προγραμματισμού με τύπους. Τα συναρτησιακά και τα βεβαιωτικά (assertive) "μέρη του λόγου" της γλώσσας της λογικής ανακλούν αυτόν τον χωρισμό του σύμπαντος με τύπους, ακόμα και στο συντακτικό επίπεδο: η αντικατάσταση και το πέρασμα παραμέτρων μπορούν να γίνουν μόνο με αυτόν τον τρόπο, σεβόμενοι τους "τύπους". (el) Sortenlogik entspringt der Intention, das (mengentheoretische) Universum (Grundmenge, Allklasse, bis hin zu einem Grothendieck-Universum) nicht als eine homogene Ansammlung von (mathematischen) Objekten zu betrachten, sondern diese auf verschiedene Klassen oder Typen aufzuteilen, die in diesem Zusammenhang Sorten genannt werden (ähnlich wie die Datentypen in vielen Programmiersprachen und Datenbanksystemen). Jedem Term einer logischen Formel wird eine Sorte zugeordnet. Unifikation von Termen ist nur dann zugelassen, wenn beide Terme von der gleichen Sorte sind; Substitution und Argumentübergabe können ebenfalls nur unter Berücksichtigung dieser Sorten erfolgen. Falsche Sortenzuordnungen werden also bereits als Syntaxfehler ausgewiesen. (de) Many-sorted logic can reflect formally our intention not to handle the universe as a homogeneous collection of objects, but to partition it in a way that is similar to types in typeful programming. Both functional and assertive "parts of speech" in the language of the logic reflect this typeful partitioning of the universe, even on the syntax level: substitution and argument passing can be done only accordingly, respecting the "sorts". * a set of sorts, S * an appropriate generalization of the notion of signature to be able to handle the additional information that comes with the sorts. (en) A lógica polissortida pode refletir formalmente a nossa intenção de não lidar com o universo como um conjunto homogêneo de objetos, mas particionar isso de uma maneira que é semelhante aos de tipos em linguagens tipadas. Ambos funcionais e assertivas "partes do discurso" na linguagem da logica refletem essa partição tipificada do universo, mesmo no nível de sintaxe: substituição e argumento de passagem só pode ser feito em conformidade, respeitando os "tipos". O universo de discurso de qualquer estrutura dessa assinatura é então fragmentada em subconjuntos dijuntos, um para cada tipo. (pt) |
| rdfs:label | Sortenlogik (de) Λογική με πολλούς τύπους (el) Many-sorted logic (en) Lógica polissortida (pt) |
| owl:sameAs | freebase:Many-sorted logic yago-res:Many-sorted logic wikidata:Many-sorted logic dbpedia-de:Many-sorted logic dbpedia-el:Many-sorted logic dbpedia-pt:Many-sorted logic https://global.dbpedia.org/id/2AxRB |
| prov:wasDerivedFrom | wikipedia-en:Many-sorted_logic?oldid=1119199895&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Sort_hierarchy.png |
| foaf:isPrimaryTopicOf | wikipedia-en:Many-sorted_logic |
| is dbo:wikiPageDisambiguates of | dbr:Sort dbr:Sorted |
| is dbo:wikiPageRedirects of | dbr:Sortedness dbr:Order-sorted_logic dbr:Many_sorted_logic |
| is dbo:wikiPageWikiLink of | dbr:Algebraic_semantics_(computer_science) dbr:Cylindric_algebra dbr:E_(theorem_prover) dbr:List_of_mathematical_logic_topics dbr:SRI_International dbr:Constructive_set_theory dbr:Leon_Henkin dbr:Structure_(mathematical_logic) dbr:Gödel_(programming_language) dbr:Term_(logic) dbr:HiLog dbr:Higher-order_logic dbr:Sortedness dbr:Second-order_arithmetic dbr:Sort dbr:Sorted dbr:Extensions_of_First_Order_Logic dbr:System_U dbr:Non-classical_logic dbr:Order-sorted_logic dbr:Many_sorted_logic |
| is foaf:primaryTopic of | wikipedia-en:Many-sorted_logic |
