Formal sys-Pradicate semantic

本文主要是介绍Formal sys-Pradicate semantic，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

介绍个定义

Interpretation $\mathcal{D}$
已知有$\sum$ 是一阶谓词逻辑(PL1)的Signatur
那么我们定义这个Signatur的interpretation $\mathcal{D}$为(D,I)，并且具有以下性质：
1.D是任意的非空的集合
2.I是Signatur符号的映射：
1).对任意常数c有:I(c) $\in$ D
2).n>=1,对于有n个参数的函数符号f有:I(f):$D^n \to D$
3).对于任意不含有参数的谓词符号 P有:I(P) $\in$ {T,F}
4).n>=1,对于任意的含有n个参数的谓词符号p存在对应的一个n阶关系I(p) $\subseteq D^n$
断言(Variablenbelegung)$\beta$
$\beta$:Var $\to$D.
已知有x$\in$Var d$\in$D,那么使x取d值的断言为：

$$\text{$\beta_x^d(y)$} \begin{cases} d&falls\text{ } y=x\\ \text{$\beta$(y)}&falls\text{ } y\text{$\neq$}x \end{cases}$$
//已知x取d值，那么关于变量y的断言是：如果x=y，那么结果就是d，而如果x不等于y，那么关于y的断言还是未知，用 $\beta(y)$表示

评价Formel(Auswertungsfunktion):

已知(D,I)是$\sum$的Interpretation，$\beta$是关于D的断言。那么我们定义一个评价函数$Val_{D,I,\beta}$，并且他满足以下属性：
$val_{D,I,\beta}(t) \in D$ 当$t \in Term_\sum$
$val_{D,I,\beta}(A) \in${T,F} 当A$\in For_\sum$
$val_{D,I,\beta}(x)=\beta(x) 其中x \in Var$
$val_{D,I,\beta}(f(t_1,...,t_n))=(I(f))(val_{D,I,\beta}(t_1),...,val_{D,I,\beta}(t_n))$
1.
$val_{D,I,\beta}(1)=T$
$val_{D,I,\beta}(0)=F$

$$val_{D,I,\beta}(s\doteq t):= \begin{cases} T&当val_{D,I,\beta}(s)=val_{D,I,\beta}(t)\\ F&其他 \end{cases}$$
$val_{D,I,\beta}(P):=I(P)$ 其中P不包含参数的谓词符号
$$val_{D,I,\beta}(p(t_1,...,t_n)):= \begin{cases} T&当(val_{D,I,\beta}(t_1),...,val_{D,I,\beta}(t_n)) \in I(p)\\ F&其他 \end{cases}$$
//有点问号？？？
2. $val_{D,I,\beta}(X)其中X \in${ $\lnot A,A\land B,A \lor B, A \to B, A \leftrightarrow B$}的情况和表达逻辑的相同
3. $$val_{D,I,\beta}(\forall xA):= \begin{cases} T&当对于所有的d\in D有val_{D,I,\beta_x^d}(A)=T\\ F&其他 \end{cases}$$
4. $$val_{D,I,\beta}(\exists x A):= \begin{cases} T&当存在一个d \in D满足val_{D,I,\beta_x^d}(A)=T\\ F&其他 \end{cases}$$
等价定理
已知有 $\mathcal{D}$是一个Interpretation， $\beta,\gamma$是两个变量断言(Variablenbelegung),那么就有：
1.已知 $\beta(x)=\gamma(x)$其中 $x \in Var(t),t为Term$,可以推出： $val_{\mathcal{D},\beta}(t)=val_{\mathcal{D},\gamma}(t)$
2.已知针对Formel A有 $\beta(x)=\gamma(x)$其中x $\in Frei(A)$,那么可以推出 $val_{\mathcal{D},\beta}(A)=val_{\mathcal{D},\beta}(A)$
3.如果 $A \in For_\sum$是封闭的，那么就有 $val_{\mathcal{D},\beta}(A)=val_{\mathcal{D},\gamma}(A)$

算数结构(Arithmetic structure)

Signatur $\sum_{arith}=${0,1,*,+,<}
在这里要认识两种结构，一种是普通的数学整数结构，在这里就跳了，另一种是Java的整数结构(就是有溢出的那种)他表示如下：
$\mathcal{Z}_{Jint}=(\mathbb{Z},*,+,<)$
$\mathbb{Z}_{Jint}:=$[int_MIN,int_MAX]=[$-2^{32},2^{32}-1$]
n+m:=int_MIN+(int_HALFRANGE+(n+m))%int_RANGE
n*m:=int_MIN+(int_HALFRANGE+(n*m))%int_RANGE
其中：int_HALFRANGE=$2^{31}$ int_RANGE=$2^{32}$
$\Rightarrow$
int_MAX+1=int_MIN
int_MIN+(-1)=int_MAX
比较$\mathbb{Z}和\mathbb{Z}_{Jint}$

$$\begin{array}{c|c|c} \hline Formel \varnothing &\mathcal{Z}\models\varnothing&\mathcal{Z}\models\varnothing\\ \hline \forall x\exists y(x<y)&yes&no\\ \hline \forall x\forall y((x+1)*y)=x*y+y)&yes&yes\\ \hline \exists x(0<x \land x+1 <0)&no&yes\\ \hline \end{array}$$

Term的替换原则(Substitutionslemma)

已知$\sum$是一个Signatur，$\mathcal{D}$是对$\sum$的一个Interpretation，$\beta,\beta'$是两个断言，$\sigma$是一个替换，那么就有：
$val_{\mathcal{D},\beta}(\sigma(t))=val_{\mathcal{D},\beta'}(t)$
其中对于所有的变量x$\in Var$有：
$\beta'(x)=val_{\mathcal{D},\beta}(\sigma(x))$
//也就是说$\beta'(x)=\beta(\sigma(x))$吗
证明：略//呵呵呵呵呵呵呵呵呵呵呵？？？？
//另外上述原则同时适用于不含冲突的替换证明同略？？？

Hoare 赋值规则

Hoare是一个三元式,分别为前置条件、操作、后置条件，其赋值规则表达如下：
{{x/s}A} x:=s {A}
可以这么理解，如果前置条件为真，那么进行赋值操作(就是替换了，把x替换为s)，那么得到的相应的结果也为真。
由上述规则可以推出：
已知$\sum$是一个Signatur，$\mathcal{D}$是针对$\sum$的一个Interpretation，$\beta$是一个断言，$\sigma$是一个无冲突的替换其中对于所有的不等于x的变量y满足$\sigma(y)=y$。那么就有：
$val_{\mathcal{D},\beta}(\forall xA \to \sigma(A))=W$
$val_{\mathcal{D},\beta}(\sigma(A) \to \exists xA)=W$
证明看不懂

Model

以下有关仅用于不含有自由变量的Formel。
我们说针对一个$\sum$的Interpretation是一个关于不含有自由变量的Formel A的Model，当$val_\mathcal{D}(A)=T$.
对Formel集合的Model的定义与此类似：要求集合中的每一个Formel B都满足$val_\mathcal{B}=T$.

推出$\vDash$

已知有：$M \in For_\sum,A \in For_\sum$并且两者都不含有自由变量，那么有：
$M \vDash_\sum A :\Leftrightarrow$M中的每一个Model，同时也是A的Model$:\Leftrightarrow M \cup${$\lnot A$}没有Model
我们就说由M可以推出M或者A跟随M(Aus M folgt A)
一些简化表达：
用$\vDash$代替$\vDash_\sum$
用$\vDash A$代替$\varnothing \vDash A$
用$B \vDash A$代替{B}$\vDash A$

普遍成立

$A \in For_\sum$是：
普遍成立的(allgemeingültig)当且仅当 $\vDash A$
可实现的(erfüllbar)当且仅当 $\lnot A$不是普遍成立的
1.下面的说法是等价的：
1).A 是普遍成立的
2).A的每一个Interpretation都是Model
3).对于所有的$\mathcal{D}$有$val_\mathcal{D}(A)=T$
2.下面说法也是等价的：
1).A是可实现的
2).存在$\mathcal{D}$满足$val_\mathcal{D}(A)=W$
一些普遍成立的Formel
$$
1.\lnot \forall xA \leftrightarrow \exists x \lnot A \
2.\lnot \exists xA \leftrightarrow \forall x \lnot A \
3.\forall x \forall y A \leftrightarrow \forall y \forall x A \
4.\exists x \exists y A \leftrightarrow \exists y \exists x A \
5.\forall x(A \land B) \leftrightarrow \forall A \land \forall B \
6.\exists x(A \lor B) \leftrightarrow \exists x A \lor \exists x B \

$$

这篇关于Formal sys-Pradicate semantic的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！

---