徽标
联盟百科
通讯
下载应用,请到 Google Play
新! 在您的Android™设备上下载联盟百科!
下载
比浏览器更快的访问!
 

形式语义学

指数 形式语义学

在计算理论中,形式语义学是关注计算的模式和程序设计语言的含义的严格的数学研究的领域。 语言的形式语义是用数学模型去表达该语言描述的可能的计算来给出的。 形式语义学(formal semantics),是程序设计理论的组成部分,以数学为工具,利用符号和公式,精确地定义和解释计算机程序设计语言的语义,使语义形式化的学科。 提供程序设计语言的形式语义的方法很多,其中主要类别有:.

9 关系: 域理论公理语义学编程语言计算计算理论SECD抽象机指称语义操作语义学数学模型

域理论

域理论是研究通常叫做域(domain)的特定种类偏序集合的数学分支。因此域理论可以被看作是序理论的分支。这个领域主要应用于计算机科学中,特别是针对函数式编程语言,用它来指定指称语义。域理论以非常一般化的方式形式化了逼近和收敛的直觉概念,并与拓扑学有密切联系。在计算机科学中指称语义的一个可作为替代的方式是度量空间。.

新!!: 形式语义学和域理论 · 查看更多 »

公理语义学

公理语义学(Axiomatic semantics)是使用数理逻辑来证明程序正确性。程序中的命令的意义描述是通过对程序状态的断言(assertion)效果。断言是逻辑语句——带变量的谓词,而这些变量定义了程序的状态。 公理语义学的一个实例是霍尔逻辑。.

新!!: 形式语义学和公理语义学 · 查看更多 »

编程语言

编程语言(programming language),是用来定义计算机程序的形式語言。它是一种被标准化的交流技巧,用来向计算机发出指令。一种计算机语言让程序员能够准确地定义计算机所需要使用的数据,并精确地定义在不同情况下所应当采取的行动。 最早的编程语言是在電腦發明之前產生的,當時是用來控制及自動演奏鋼琴的動作。在電腦領域已發明了上千不同的编程語言,而且每年仍有新的编程語言誕生。很多编程語言需要用指令方式說明計算的程序,而有些编程語言則屬於宣告式編程,說明需要的結果,而不說明如何計算。 编程语言的描述一般可以分為及語義。語法是說明編程語言中,哪些符號或文字的組合方式是正確的,語義則是對於編程的解釋。有些語言是用規格文件定義,例如C語言的規格文件也是ISO標準中一部份,2011年後的版本為ISO/IEC 9899:2011,而其他55語言(像Perl)有一份主要的文件,視為是。.

新!!: 形式语义学和编程语言 · 查看更多 »

计算

計算(Calculation)是一種將「單一或多個的輸入值」轉換為「單一或多個的結果」的一種思考過程。 計算的定義有許多種使用方式,有相當精確的定義,例如使用各種算法進行的「算术」,也有較為抽象的定義,例如在一場競爭中「策略的計算」或是「計算」兩人之間關係的成功機率。 將7乘以8(7x8)就是一種簡單的算術。 利用布莱克-斯科尔斯模型(Black-Scholes Model)來算出財務評估中的公平價格(fair price)就是一種複雜的算術。 從投票意向計算評估出的選舉結果(民意調查)也包含了某種算術,但是提供的結果是「各種可能性的範圍」而不是單一的正確答案。.

新!!: 形式语义学和计算 · 查看更多 »

计算理论

计算理论(Theory of computation)是數學的一個領域,和计算机有密切关系。其中的理论是现代密码协议、计算机设计和许多应用领域的基础。该领域主要关心三个方面的问题:.

新!!: 形式语义学和计算理论 · 查看更多 »

SECD抽象机

SECD 机是非常有影响的意图作为函数式编程语言编译器目标的虚拟机。SECD 分别是这个机器的内部寄存器的名字的首字母:Stack, Environment, Code, Dump。这些寄存器指向在内存中链表。 这种机器最初明确设计用来计算 lambda 演算表达式。最初 Peter J. Landin 在1963年把它作为他的 ISWIM编程语言定义的一部分描述。Landin 出版的描述非常抽象,(象一种操作语义那样)留下很多实现选择开放着。所以 SECD 机经常以更具体的形式出现,比如 Peter Henderson 的 Lispkit Lisp 编译器,它自1980年开始发行。此后它已经被用做多个其他实验编译器的目标。 在1989年在卡尔加里大学的研究者制作了这种机器的一个硬件实现。.

新!!: 形式语义学和SECD抽象机 · 查看更多 »

指称语义

在计算机科学中,指称语义(Denotational semantics)是通过构造表达其语义的(叫做指称(denotation)或意义的)数学对象来形式化计算机系统的语义的一种方法。编程语言的形式语义的其他方法包括公理语义和操作语义。指称语义方式最初开发来处理一个单一计算机程序定义的系统。后来领域扩展到了由多于一个程序构成的系统,比如网络和并发系统。 指称语义起源于 克里斯托弗·斯特雷奇 和 Dana Scott 在1960年代的工作。在 Strachey 和 Scott 最初开发的时候,指称语义把计算机程序的指称(意义)解释为映射输入到输出的函数。后来证明对于允许包含递归定义的函数和数据结构,这样的元素的程序的指称(意义)定义太受限制了。为了解决这个困难,Scott 介入了基于域的指称语义的一般性方法。后来的研究者介入了基于幂域的方法,来解决并发系统的语义的问题。 粗略的说,指称语义关注找到代表程序所做所为的数学对象。这种对象的搜集叫做域。例如,程序(或程序段)可以被偏函数,或演员事件图想定,或用环境和系统之间的博弈表示: 它们都是域的一般性例子。 指称语义的一个重要原则是“语义应当是复合性的”: 程序段的指称应当建立自它的子段的指称。最简单的例子是: “3 + 4”的意义确定自“3”、“4”和“+”的意义。 指称语义最初被开发为把函数式和顺序式程序建模为映射输入到输出的数学函数的框架。本文第一节描述在这个框架内开发的指称语义。后续章节处理多态、并发等问题。.

新!!: 形式语义学和指称语义 · 查看更多 »

操作语义学

操作语义学是计算机科学中的一个概念,它是使得计算机程序在数学上更加严谨的一种手段。其它类似的手段包括提供形式语义学,包括公理语义学和指称语义。 一个计算机语言的操作语义描述一段合理的程序是怎样被理解为一系列计算机步骤的。这些步骤就是这个程序的意义。在函數程式語言中一段终结性的序列在最后一步的返回程序的值。(由于一个程序可能是非非決定的,一般来说一个程序能够有许多不同的计算步骤和许多不同的返回值。) 操作语义最早被用来定义Algol 68的语义。下面这句话引用修正的ALGOL 68报告: 一个使用严格语言编写的程序的意义是通过一个假设的计算机来执行该程序的组成部分时完成的行动来解释的。(Algol68,第二章) 丹纳·司科特是第一个在今天的这个定义下使用操作语义这个概念的(Plotkin04b)。以下是司科特关于形式语义学的讲稿,其中他提到了语义的“操作”观点。 把目光注意使得语义在更‘抽象’和更‘清晰’可以,但是假如把操作方面完全忽略的话这个计划毫无用处。(Scott70).

新!!: 形式语义学和操作语义学 · 查看更多 »

数学模型

數學模型是使用數學概念和語言來对一個系統的描述。建立数学模型的过程叫做数学建模。數學模型不只用在自然科學(如物理、生物學、地球科學、大氣科學)和工程学科(如计算机科学,人工智能)上,也用在社會科學(如經濟學、心理學、社會學和政治科學)上;其中,物理學家、工程師、统计学家、運籌學分析家和經濟學家們最常使用數學模型。模型会帮助解释一个系统,研究不同组成部分的影响,以及对行为做出预测。 Eykhoff定義「數學模型」為「對一個現存(或被建構的)系統本質的表述,以能以有用的形式表示出此系統的知識來。」 數學模型可以有許多種的形式,不只限定在動態系統、概率模型、微分方程或賽局模型而已。不同的模型可能有相同的形式,同一個模型也可能包含了不同的抽象結構。.

新!!: 形式语义学和数学模型 · 查看更多 »

重定向到这里:

形式语义程序语义

传出传入
嘿!我们在Facebook上吧! »