| dbo:abstract
|
- في المعلوماتية النظرية، علم الدلالة الشكلي formal semantics هو الحقل الذي يهتم بالدراسة الرياضية البحتة لمعنى لغات البرمجة ونماذج التحسيب. يعطى علم الدلالة الشكلي للغة ما عن طريق نموذج رياضي يصف طرق التحسيب الممكنة التي توصف بهذه اللغة. (ar)
- Sémantika programovacích jazyků je v obor zabývající se důsledným matematickým popisem významu programovacího jazyka. Zhodnocuje význam syntakticky platných řetězců v daném programovacím jazyce, včetně jejich výpočtu. V případě ohodnocování syntakticky neplatných řetězců, není výpočet proveden. Sémantika popisuje procesy, které řídí počítač při vykonávání programu v daném programovacím jazyce. Například tím, že popisuje vztah mezi vstupem a výstupem programu, nebo popisem jak program poběží na určité platformě, tedy vytvořením modelu výpočtu. (cs)
- Στη θεωρητική πληροφορική, η τυπική σημασιολογία (formal semantics) είναι το πεδίο που ασχολείται με την αυστηρή μαθηματική μελέτη της σημασίας των γλωσσών προγραμματισμού και των υπολογιστικών μοντέλων. Η τυπική σημασιολογία μιας γλώσσας μπορεί να δοθεί από ένα μαθηματικό μοντέλο που περιγράφει τους πιθανούς υπολογισμούς που περιγράφονται από τη γλώσσα. Υπάρχουν πολλές προσεγγίσεις στην τυπική σημασιολογία, οι οποίες ανήκουν στις εξής τρεις μεγάλες κλάσεις:
* Δηλωτική σημασιολογία (Denotational semantics), στην οποία κάθε φράση της γλώσσας μεταφράζεται σε μια δήλωση (denotation), δηλ. σε μια φράση σε κάποια άλλη γλώσσα. Η δηλωτική σημασιολογία αντιστοιχεί γενικά στη μεταγλώττιση, αν και η τελική γλώσσα είναι συνήθως κάποιος μαθηματικός φορμαλισμός και όχι άλλη μια γλώσσα προγραμματισμού υπολογιστών. Για παράδειγμα, η δηλωτική σημασιολογία των συναρτησιακών γλωσσών συνήθως μεταφράζει τη γλώσσα στη θεωρία πεδίων (domain theory).
* Λειτουργική σημασιολογία (Operational semantics), στην οποία η εκτέλεση της γλώσσας περιγράφεται άμεσα (και όχι μέσω μετάφρασης). Η λειτουργική σημασιολογία γενικά αντιστοιχεί στη διερμηνεία, αν και πάλι η "γλώσσα υλοποίησης" του διερμηνέα είναι συνήθως κάποιος μαθηματικός φορμαλισμός. Η λειτουργική σημασιολογία μπορεί να ορίζει κάποια αφηρημένη μηχανή (abstract machine) και να δίνει νόημα σε φράσεις αποδίδοντάς τους τις μεταβάσεις που προκαλούν στις καταστάσεις της μηχανής. Εναλλακτικά, όπως με τον καθαρό λ-λογισμό, η λειτουργική σημασιολογία μπορεί να οριστεί μέσω συντακτικών μετασχηματισμών σε φράσεις της ίδιας της γλώσσας.
* Αξιωματική σημασιολογία (Axiomatic semantics), η οποία δίνει νόημα σε φράσεις περιγράφοντας τα λογικά αξιώματα που εφαρμόζονται σε αυτές. Η αξιωματική σημασιολογία δε διακρίνει μεταξύ του νοήματος μιας φράσης και των λογικών προτάσεων που την περιγράφουν: το νόημά της είναι ακριβώς ότι μπορεί να αποδειχτεί για αυτή σε κάποια λογική. Το κλασικό παράδειγμα αξιωματικής σημασιολογίας είναι η . Τα όρια μεταξύ των παραπάνω κλάσεων μερικές φορές μπορεί να είναι δυσδιάκριτα αλλά όλες οι γνωστές προσεγγίσεις στην τυπική σημασιολογία χρησιμοποιούν κάποια από τις παραπάνω τεχνικές ή ένα συνδυασμό τους. Εκτός από την επιλογή μεταξύ δηλωτικής, λειτουργικής και αξιωματικής σημασιολογίας, η ποικιλία στα συστήματα τυπικής σημασιολογίας οφείλεται και στην επιλογή του μαθηματικού φορμαλισμού που θα χρησιμοποιηθεί σαν υπόβαθρο. Κάποιες παραλλαγές της τυπικής σημασιολογίας περιλαμβάνουν τα εξής:
* Η σημασιολογία δράσεων (action semantics), είναι μια προσέγγιση που προσπαθεί να οργανώσει τη δηλωτική σημασιολογία, χωρίζοντας τη διαδικασία τυποποίησης σε δύο επίπεδα (μάκρο- και μίκρο- σημασιολογία) και προκαθορίζει τρεις σημασιολογικές οντότητες (ενέργειες, δεδομένα και yielders) για την απλοποίηση της προδιαγραφής.
* Η αλγεβρική σημασιολογία (algebraic semantics) περιγράφει τη σημασιολογία με όρους από άλγεβρες.
* Οι γραμματικές ιδιοτήτων (attribute grammars) ή κατηγορηματικές γραμματικές ορίζουν συστήματα που υπολογίζουν συστηματικά "μεταδεδομένα" (που αποκαλούνται ιδιότητες ή attributes) για τις διάφορες περιπτώσεις της σύνταξης μιας γλώσσας. Οι γραμματικές ιδιοτήτων μπορούν να θεωρηθούν δηλωτική σημασιολογία στην οποία η τελική γλώσσα είναι απλά η αρχική γλώσσα με την προσθήκη σημειώσεων για τις ιδιότητες. Εκτός από την τυπική σημασιολογία, οι γραμματικές ιδιοτήτων έχουν επίσης χρησιμοποιηθεί για την παραγωγή κώδικα σε μεταγλωττιστές και για να προστεθούν συνθήκες με συμφραζόμενα (context-sensitive) σε κανονικές γραμματικές ή γραμματικές χωρίς συμφραζόμενα.
* Η κατηγορηματική σημασιολογία (categorical semantics ή functorial semantics) χρησιμοποιεί τη θεωρία κατηγοριών σαν τον κεντρικό της μαθηματικό φορμαλισμό.
* Η σημασιολογία του ταυτοχρονισμού (concurrency semantics) είναι ένας όρος που εφαρμόζεται σε κάθε τυπική σημασιολογία που περιγράφει ταυτόχρονους υπολογισμούς. Ιστορικά σημαντικοί ταυτόχρονοι φορμαλισμοί είναι το και οι (process calculi).
* Η σημασιολογία παιγνίων (game semantics) χρησιμοποιεί μια μεταφορά εμπνευσμένη από τη θεωρία παιγνίων.
* Η σημασιολογία μετασχηματισμού κατηγορημάτων (predicate transformer semantics), που αναπτύχθηκε από τον Έντσγκερ Ντάικστρα, περιγράφει τη σημασία ενός τμήματος ενός προγράμματος σαν τη συνάρτηση που μετασχηματίζει μια μετασυνθήκη (postcondition) στην προσυνθήκη (precondition) που χρειάζεται για τη λειτουργία του. Υπάρχουν πολλοί λόγοι για τους οποίους κάποιος θα ήθελε να περιγράψει τις σχέσεις μεταξύ των διάφορων τυπικών σημασιολογιών. Για παράδειγμα:
* Μπορεί να θέλει να αποδείξει ότι κάποια συγκεκριμένη λειτουργική σημασιολογία μιας γλώσσας ικανοποιεί τις λογικές προτάσεις μιας αξιωματικής σημασιολογίας της γλώσσας αυτής. Μια τέτοια απόδειξη δείχνει ότι είναι "ορθό" ("sound") να χρησιμοποιηθεί λογικά μια συγκεκριμένη (λειτουργική) στρατηγική διερμηνείας χρησιμοποιώντας ένα συγκεκριμένο (αξιωματικό) σύστημα αποδείξεων.
* Δεδομένης μιας γλώσσας, μπορεί να θέλει να ορίσει μια αφηρημένη μηχανή υψηλού επιπέδου και μια χαμηλού επιπέδου, ώστε η τελευταία να περιέχει περισσότερες πρωτογενείς λειτουργίες από την πρώτη. Στη συνέχεια μπορεί να αποδείξει ότι μια λειτουργική σημασιολογία της μηχανής υψηλού επιπέδου σχετίζεται μέσω με τη σημασιολογία της μηχανής χαμηλού επιπέδου. Μια τέτοια απόδειξη απαιτεί η μηχανή χαμηλού επιπέδου να "υλοποιεί πιστά" τη μηχανή υψηλού επιπέδου. Πολλαπλές σημασιολογίες μπορούν μερικές φορές να συσχετιστούν με τη χρήση αφαίρεσης, μέσω της θεωρίας της . Το πεδίο της τυπικής σημασιολογίας περιλαμβάνει όλα τα ακόλουθα:
* Τον ορισμό των σημασιολογικών μοντέλων.
* Τις σχέσεις μεταξύ διαφορετικών σημασιολογικών μοντέλων.
* Τις σχέσεις μεταξύ διαφορετικών προσεγγίσεων της σημασίας.
* Τη σχέση μεταξύ υπολογισμού και των βασικών μαθηματικών δομών από πεδία όπως η λογική, η θεωρία συνόλων, η θεωρία μοντέλων, η θεωρία κατηγοριών, κλπ. Συνδέεται στενά με άλλες περιοχές της επιστήμης των υπολογιστών όπως η σχεδίαση γλωσσών προγραμματισμού, η θεωρία τύπων, οι μεταγλωττιστές, οι διερμηνείς, η και ο έλεγχος μοντέλων. (el)
- Formale Semantik beschäftigt sich mit der exakten Bedeutung von Termen in künstlichen oder natürlichen Sprachen. Dabei kann sowohl die Bedeutung in bestehenden Sprachen untersucht als auch die Bedeutung in neu geschaffenen Sprachen festgelegt werden. In Abgrenzung zur Semantik im allgemeinen Sinn, wie sie vor allem in Philosophie und Linguistik betrieben wird, arbeitet die formale Semantik mit rein formalen, logisch-mathematischen Methoden. Formale Semantik wird in der Logik, in der Informatik und in der Linguistik betrieben. Wegen der Wichtigkeit exakter Bedeutungstheorien für die genannten drei Disziplinen und wegen unterschiedlicher Schwerpunkte und Zielsetzungen – teils auch wegen unterschiedlicher Methoden – hat jede dieser Wissenschaften heute ein eigenes Teilgebiet, das als formale Semantik bezeichnet wird. Die formale Semantik in Logik, jene in Informatik und die formale Semantik in Linguistik sind jedoch in vielerlei Hinsicht miteinander verflochten und greifen häufig ineinander bzw. auf die Ergebnisse der jeweils anderen zurück. Die moderne formale Semantik hat ihren Ursprung in Arbeiten von Alfred Tarski, Richard Montague, Alonzo Church und anderen. (de)
- En la Teoría de lenguajes de programación, la semántica es el campo que tiene que ver con el estudio riguroso desde un punto de vista matemático del significado de los lenguajes de programación. Esto se hace evaluando el significado de cadenas sintácticamente legales definidas por un lenguaje de programación específico, mostrando el proceso computacional involucrado. En el caso de que la evaluación fuera de cadenas sintácticamente ilegales, el resultado sería no-cómputo. La semántica describe el proceso que una computadora sigue cuando ejecuta un programa en ese lenguaje específico. Esto se puede mostrar describiendo la relación entre la entrada y la salida de un programa, o una explicación de cómo el programa se ejecutará en cierta plataforma, y consecuentemente creando un modelo de computación. Semánticas formales ayudan, por ejemplo, a escribir compiladores, a tener un mejor entendimiento de lo que un programa está haciendo y a hacer determinadas pruebas, como demostrar que el siguiente código if 1 == 1 then S1 else S2 tiene el mismo efecto que S1 por sí solo. (es)
- En informatique théorique, la sémantique formelle (des langages de programmation) est l’étude de la signification des programmes informatiques vus en tant qu’objets mathématiques. (fr)
- In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax. Semantics describes the processes a computer follows when executing a program in that specific language. This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will be executed on a certain platform, hence creating a model of computation. (en)
- プログラム意味論（プログラムいみろん、英: program semantics）とは、計算機科学（特に理論計算機科学と分類されることもある）の一分野で、プログラミング言語の意味と計算モデルに関する分野である。形式的なものは、プログラミング言語の形式意味論とも呼ばれる。標準規格等では形式的でなく意味論を与えているものも多い。 (ja)
- Nel campo dell'informatica teorica, il termine semantica formale riguarda i modelli matematici che definiscono formalmente i linguaggi di programmazione o, più generalmente, la computazione stessa. Esistono molteplici approcci allo studio di queste semantiche; i quali ricadono in 3 categorie principali: 1.
* La semantica denotazionale; che si preoccupa di formalizzare l'esecuzione delle istruzioni di un linguaggio di programmazione utilizzando degli oggetti matematici, chiamati denotazioni, che ne descrivono il significato e quindi l'esecuzione. In genere questa semantica dev'essere composizionale: la denotazione di una parte del programma dev'essere costruita partendo da sue sotto istruzioni. 2.
* La semantica operazionale; che descrive l'esecuzione di un programma attraverso transizioni definite direttamente sul linguaggio del programma. Questo tipo di formalismo è concettualmente simile all'interpretazione vera e propria in cui abbiamo una macchina astratta e le istruzioni applicano transizioni di stato in questa macchina. Abbiamo dunque una sequenza di passi computazionali definita per ogni programma (che può essere non deterministica) e che viene generata solitamente con l'applicazione di un insieme di regole di inferenza sull'insieme delle istruzioni stesso. 3.
* La ; che come la precedente si basa sul contraddistinguere lo stato della computazione ma utilizza dei predicati logici per definire lo stato attuale. Questo tipo di semantica non distingue la verità implicata da una parte di codice ed il significato dello stesso: sono esattamente la stessa cosa. In genere si utilizza per cercare di verificare la correttezza dei programmi ed il suo esempio più lampante e classico è la logica di Hoare (it)
- Semântica formal é a área de estudo de ciência da computação que se preocupa em especificar o significado (ou comportamento) de programas de computador e partes de hardware. A semântica é complementar à sintaxe de programas de computador, que se preocupa em descrever as estruturas de uma linguagem de programação. A necessidade de uma semântica formal (matemática) para linguagens de programação justifica-se, pois:
* Pode revelar ambiguidades na definição da linguagem (o que uma descrição informal não permitiria revelar);
* É uma base para implementação (síntese), análise e verificação formal. (pt)
- Семантика в теорії програмування — розділ, що вивчає математичне значення мови програмування та моделі обчислень. Формальна семантика мови задається математичною моделлю яка описує обчислення можливі в мові . (uk)
- Сема́нтика в программировании — дисциплина, изучающая формализации значений конструкций языков программирования посредством построения их формальных математических моделей. В качестве инструментов построения таких моделей могут использоваться различные средства, например, математическая логика, λ-исчисление, теория множеств, теория категорий, теория моделей, универсальная алгебра. Формализация семантики языка программирования может использоваться как для описания языка, определения свойств языка, так и для целей формальной верификации программ на этом языке программирования. (ru)
- 在计算理论中，形式语义学是关注计算的模式和程序设计语言的含义的严格的数学研究的领域。 语言的形式语义是用数学模型去表达该语言描述的可能的计算来给出的。 形式语义学（formal semantics），是程序设计理论的组成部分，以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义，使语义形式化的学科。 提供程序设计语言的形式语义的方法很多，其中主要类别有：
* 指称语义学，着重于语言的执行结果而非过程，包括域理论；
* 操作语义学，例如抽象机（象SECD抽象机），着重于描述语言的过程；
* 公理语义学，如 和。 (zh)
|
| rdfs:comment
|
- في المعلوماتية النظرية، علم الدلالة الشكلي formal semantics هو الحقل الذي يهتم بالدراسة الرياضية البحتة لمعنى لغات البرمجة ونماذج التحسيب. يعطى علم الدلالة الشكلي للغة ما عن طريق نموذج رياضي يصف طرق التحسيب الممكنة التي توصف بهذه اللغة. (ar)
- Sémantika programovacích jazyků je v obor zabývající se důsledným matematickým popisem významu programovacího jazyka. Zhodnocuje význam syntakticky platných řetězců v daném programovacím jazyce, včetně jejich výpočtu. V případě ohodnocování syntakticky neplatných řetězců, není výpočet proveden. Sémantika popisuje procesy, které řídí počítač při vykonávání programu v daném programovacím jazyce. Například tím, že popisuje vztah mezi vstupem a výstupem programu, nebo popisem jak program poběží na určité platformě, tedy vytvořením modelu výpočtu. (cs)
- En informatique théorique, la sémantique formelle (des langages de programmation) est l’étude de la signification des programmes informatiques vus en tant qu’objets mathématiques. (fr)
- In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax. Semantics describes the processes a computer follows when executing a program in that specific language. This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will be executed on a certain platform, hence creating a model of computation. (en)
- プログラム意味論（プログラムいみろん、英: program semantics）とは、計算機科学（特に理論計算機科学と分類されることもある）の一分野で、プログラミング言語の意味と計算モデルに関する分野である。形式的なものは、プログラミング言語の形式意味論とも呼ばれる。標準規格等では形式的でなく意味論を与えているものも多い。 (ja)
- Semântica formal é a área de estudo de ciência da computação que se preocupa em especificar o significado (ou comportamento) de programas de computador e partes de hardware. A semântica é complementar à sintaxe de programas de computador, que se preocupa em descrever as estruturas de uma linguagem de programação. A necessidade de uma semântica formal (matemática) para linguagens de programação justifica-se, pois:
* Pode revelar ambiguidades na definição da linguagem (o que uma descrição informal não permitiria revelar);
* É uma base para implementação (síntese), análise e verificação formal. (pt)
- Семантика в теорії програмування — розділ, що вивчає математичне значення мови програмування та моделі обчислень. Формальна семантика мови задається математичною моделлю яка описує обчислення можливі в мові . (uk)
- Сема́нтика в программировании — дисциплина, изучающая формализации значений конструкций языков программирования посредством построения их формальных математических моделей. В качестве инструментов построения таких моделей могут использоваться различные средства, например, математическая логика, λ-исчисление, теория множеств, теория категорий, теория моделей, универсальная алгебра. Формализация семантики языка программирования может использоваться как для описания языка, определения свойств языка, так и для целей формальной верификации программ на этом языке программирования. (ru)
- 在计算理论中，形式语义学是关注计算的模式和程序设计语言的含义的严格的数学研究的领域。 语言的形式语义是用数学模型去表达该语言描述的可能的计算来给出的。 形式语义学（formal semantics），是程序设计理论的组成部分，以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义，使语义形式化的学科。 提供程序设计语言的形式语义的方法很多，其中主要类别有：
* 指称语义学，着重于语言的执行结果而非过程，包括域理论；
* 操作语义学，例如抽象机（象SECD抽象机），着重于描述语言的过程；
* 公理语义学，如 和。 (zh)
- Στη θεωρητική πληροφορική, η τυπική σημασιολογία (formal semantics) είναι το πεδίο που ασχολείται με την αυστηρή μαθηματική μελέτη της σημασίας των γλωσσών προγραμματισμού και των υπολογιστικών μοντέλων. Η τυπική σημασιολογία μιας γλώσσας μπορεί να δοθεί από ένα μαθηματικό μοντέλο που περιγράφει τους πιθανούς υπολογισμούς που περιγράφονται από τη γλώσσα. Υπάρχουν πολλές προσεγγίσεις στην τυπική σημασιολογία, οι οποίες ανήκουν στις εξής τρεις μεγάλες κλάσεις: Κάποιες παραλλαγές της τυπικής σημασιολογίας περιλαμβάνουν τα εξής: Το πεδίο της τυπικής σημασιολογίας περιλαμβάνει όλα τα ακόλουθα: (el)
- Formale Semantik beschäftigt sich mit der exakten Bedeutung von Termen in künstlichen oder natürlichen Sprachen. Dabei kann sowohl die Bedeutung in bestehenden Sprachen untersucht als auch die Bedeutung in neu geschaffenen Sprachen festgelegt werden. In Abgrenzung zur Semantik im allgemeinen Sinn, wie sie vor allem in Philosophie und Linguistik betrieben wird, arbeitet die formale Semantik mit rein formalen, logisch-mathematischen Methoden. Die moderne formale Semantik hat ihren Ursprung in Arbeiten von Alfred Tarski, Richard Montague, Alonzo Church und anderen. (de)
- En la Teoría de lenguajes de programación, la semántica es el campo que tiene que ver con el estudio riguroso desde un punto de vista matemático del significado de los lenguajes de programación. Esto se hace evaluando el significado de cadenas sintácticamente legales definidas por un lenguaje de programación específico, mostrando el proceso computacional involucrado. En el caso de que la evaluación fuera de cadenas sintácticamente ilegales, el resultado sería no-cómputo. La semántica describe el proceso que una computadora sigue cuando ejecuta un programa en ese lenguaje específico. Esto se puede mostrar describiendo la relación entre la entrada y la salida de un programa, o una explicación de cómo el programa se ejecutará en cierta plataforma, y consecuentemente creando un modelo de compu (es)
- Nel campo dell'informatica teorica, il termine semantica formale riguarda i modelli matematici che definiscono formalmente i linguaggi di programmazione o, più generalmente, la computazione stessa. Esistono molteplici approcci allo studio di queste semantiche; i quali ricadono in 3 categorie principali: (it)
|