Skip to content

Commit

Permalink
11.18
Browse files Browse the repository at this point in the history
  • Loading branch information
yhtq committed Nov 18, 2024
1 parent db6aa91 commit e29f154
Show file tree
Hide file tree
Showing 3 changed files with 186 additions and 30 deletions.
48 changes: 24 additions & 24 deletions 数理逻辑/main.typ
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
#let calP = $cal(P)$
#let calL = $cal(L)$
#let Interpret = $cal(I)$
#let subst(AA, PP, pp) = $AA_( PP \/ pp )$
#let subst(AA, PP, pp) = $AA_( PP \/ pp )$
#let deduction(body) = {
set enum(numbering: "(1)")
set align(left)
Expand Down Expand Up @@ -98,7 +98,7 @@
- 如果任取变元的所有赋值,该命题形式均为真,则称该命题形式为重言式/永真式
- 如果任取变元的所有赋值,该命题形式均为假,则称该命题形式为矛盾式
- 否则称该命题形式为可满足式
判断一个命题形式是否可可满足式是一个 NP 问题,该问题称为 SAT 问题
判断一个命题形式是否可可满足式是一个 NP 问题,该问题称为 SAT 问题
]
#definition[][
- 若 $calA -> calB$ 是重言式,则称 $calA$ 蕴含 $calB$,记作 $calA => calB$
Expand All @@ -115,7 +115,7 @@
这里的“反证法”是一种逻辑演算之外的证明方法。因为之前定义的赋值存在于元语言中,因此反证法也是在元语言中反证。
]
#definition[][
$calA$ 是包含变元 $p_1, p_2, ..., p_n$ 的命题形式,$calP_i, 1<=i<=n$ 是任意的命题形式,则称将 $p_i$ 替换为 $calP_i$ 的操作称为替换,记作 $subst(calA, p_i, calP_i)$
$calA$ 是包含变元 $p_1, p_2, ..., p_n$ 的命题形式,$calP_i, 1<=i<=n$ 是任意的命题形式,则称将 $p_i$ 替换为 $calP_i$ 的操作称为替换,记作 $subst(calA, p_i, calP_i)$
]
#definition[受限命题形式][
@proposition-form 中,若只用 $not1, and, or$ 作为连接符,则称其为受限命题形式
Expand All @@ -133,7 +133,7 @@
]
#theorem[常用命题逻辑定理][
以下都是重言式:
- $not1 (A and not1 A)$
- $not1 (A and not1 A)$
- $A or not1 A$
- $A <-> not1 not1 A$
- $A <-> A or A <-> A and A$
Expand Down Expand Up @@ -273,11 +273,11 @@
- #align_left[#fS => ]
+ #align_left[若 $B in Gamma$,则 $Gamma tack calA -> calB$ 显然]
+ #align_left[若 $B = A$,只需使用 $tack calA -> calA$ 即可]
- #align_left[#MP("a", "b") => (此时 $b = a -> calB$)]
- #align_left[#MP("a", "b") => (此时 $b = a -> calB$)]
由归纳法,有 $Gamma tack calA -> a, Gamma tack calA -> (a -> calB)$,只需证明:
$
{calA -> a, calA -> (a -> calB)} tack calA -> calB
$
$
来自于:
#deduction[
+ $calA -> a := fS$
Expand All @@ -287,7 +287,7 @@
+ #indent(2) $calA -> calB := #MPb(4, 1)$
]
]

]
#theorem[演绎定理2][
$Gamma tack calA -> calB$,则 $Gamma union {calA} tack calB$
Expand Down Expand Up @@ -336,7 +336,7 @@
#definition[重言式][
$v models calA$ 对任意赋值 $v$ 都成立,则称 $calA$ 是重言式,记作 $models calA$
]

== 完全性定理
前面的形式系统使用的是证明论的思想,使用 $tack$,是指纯粹语法的推断。而之前的章节从真值指派看待命题逻辑,使用的是模型论的思想,使用 $models$,指通过语义进行的分析。完全性定理即是说,这两种思想是等价的。
#theorem[命题逻辑的可靠性(soundness)][
Expand All @@ -347,8 +347,8 @@
#pattern-match[
match L with
- #align_left[#fA => 逐一验证公理都是重言式即可]
- #align_left[#MP("a", "b") => 此时 $b = a -> calB$]
由归纳法,$a, b$ 都是重言式,不难验证 $b space a : calB$ 当然也是重言式
- #align_left[#MP("a", "b") => 此时 $b = a -> calB$]
由归纳法,$a, b$ 都是重言式,不难验证 $b space a : calB$ 当然也是重言式
]
]
#theorem[命题逻辑的一致性][
Expand Down Expand Up @@ -389,7 +389,7 @@
v(calA) = T "if and only if" tack_(L^') calA
$
$L'$ 的一致完全性保证了定义是合理的。

为了证明它是赋值,只需证明:
$
v(calA -> calB) = T "if and only if" v(calA) = F "or" v(calB) = T
Expand All @@ -413,9 +413,9 @@
直觉主义逻辑由如下资料定义:
- 字符集:公式集及 ${top(真), bot(假), and, or, ->}$
- 公理模式:
#enum(numbering:
#enum(numbering:
(nums => "(I" + str(nums) + ")")

)[$calA -> (calB -> calA)$][
$(calA -> (calB -> calC)) -> ((calA -> calB) -> (calA -> calC))$
][
Expand Down Expand Up @@ -467,18 +467,18 @@
#definition[公式与项][
一阶语言中良好的表达式分为公式与项,满足文法规则:
```
term ::= x_i
| a_i
term ::= x_i
| a_i
| f_m^n (term_1, ..., term_n)
formula ::= A_m^n (term_1, ..., term_n)
| not formula
| formula -> formula
formula ::= A_m^n (term_1, ..., term_n)
| not formula
| formula -> formula
| forall x_i, formula
```
特别的:
- 只由常元和函项符构成的项称为闭项,否则称为开项。显然将一些闭项加入常元集可以得到拓展,称为闭项拓展。只用常元的拓展称为常元拓展。
- 不含量词,变元的公式称为命题公式,也就是命题逻辑语言 $language_0$ 中的公式
]
]
#lemma[][
#language 中的公式集和项集都是至多可数的
]
Expand Down Expand Up @@ -526,7 +526,7 @@
- 对于谓词符,存在一些对象满足这个谓词,而另一些不满足
- 对于函项符,它将一些对象映射为另一个对象
这应该能准确的描述一阶逻辑中的非逻辑符号的解释。这被称为 FOL 假设。

具体而言,我们可以依赖于集合论建立一阶语言的模型:
#definition[Tarski][
一个一阶语言 $language$ 的解释 $Interpret$ 包括:
Expand All @@ -549,7 +549,7 @@

为了方便,假设 $language$ 中的常元为 $a_1, ..., a_i, ...$,我们就可以记:
$
D_I = {a_i}
D_I = {a_i}
$
(如果常元不足,做常元扩展即可)\
该记法成立是因为 $D_I$ 是元语言中的集合,其中元素与记法无关,因此不妨就用 #language 中的常元符号。
Expand Down Expand Up @@ -600,7 +600,7 @@
&| calB(x_i) -> calC(x_i) => "易证"\
&| forall x_i calB(x_i) => "替换只替换自由变元,显然"\
&| forall x_j calB(x_i) => v' models calA(x_i) &&<=> "forall" d_i in D_I, v' models calB(x_i)(x_j \/ d_i)\
$
#lemmaLinear[][
$t$$calB(x_i)(x_j \/ d_i)$$x_i$ 自由,且 $calB(x_i)(x_j \/ d_i)(x_i \/ t) = calB(t)(x_j \/ d_i)$
Expand All @@ -613,7 +613,7 @@
$
&"forall" d_i in D_I, v models calB(x_i)(x_j \/ d_i)(x_i \/ t) \
&<=> "forall" d_i in D_I, v models calB(x_i)(x_j \/ d_i)(x_i \/ t) \
&<=> "forall" d_i in D_I, v models calB(t)(x_j \/ d_i)\
&<=> "forall" d_i in D_I, v models calB(t)(x_j \/ d_i)\
&<=> v models forall x_j calB(t)
$
]
Expand Down Expand Up @@ -993,7 +993,7 @@
$
无妨设 $x_i != x_j, x_1 != y_j$,则由替换定理的推论,有:
$
tack (Q_1 x_1 ... Q_n x_n calB' -> P_1 y_1 ... P_n y_n calC') <-> calA
tack (Q_1 x_1 ... Q_n x_n calB' -> P_1 y_1 ... P_n y_n calC') <-> calA
$
]
#definition[$Pi, Sigma$][
Expand Down
12 changes: 6 additions & 6 deletions 计算方法B/code/hw6/hw6.typ
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@

#ys.map(str).join(", ")

#let laugrange(x: float) = {
#let laugrange(f, x) = {
let res = 0.0
for xi in xs{
let l = 1
Expand All @@ -31,26 +31,26 @@
l *= (x - xj) / (xi - xj)
}
}
res += l * calc.sin(xi)
res += l * f(xi)
}
res
}
误差界为:
$
abs(R(x)) = abs((f^(5) (xi))/5! product_(i = 1)^5 (x - x_i)) = abs((cos xi)/5! product_(i = 1)^5 (x - x_i)) <= 1/5! product_(i = 1)^5 abs(x - x_i)
$
#let laugrange_err(x: float) = 1 / factorial(n: 5) * xs.map(xi => calc.abs(x - xi)).product()
#let laugrange_err(x) = 1 / factorial(n: 5) * xs.map(xi => calc.abs(x - xi)).product()
#let test_point = range(10).map(i => i * 3 / 20)
选取测试点为:

#test_point.map(str).join(", ")\
计算误差界分别为:

#test_point.map(x => laugrange_err(x: x)).map(str).join(", ")
#test_point.map(x => laugrange_err(x)).map(str).join(", ")

实际误差为:

#test_point.map(x => calc.abs(laugrange(x: x) - calc.sin(x))).map(str).join(", ")
#test_point.map(x => calc.abs(laugrange(calc.sin, x) - calc.sin(x))).map(str).join(", ")

可见误差界比较准确。要使最大误差小于 $10^(-10)$,注意到:
$
Expand Down Expand Up @@ -211,4 +211,4 @@

$autoRVecNF(bi, n)$ 满秩不难得到 $H$ 满秩,因此解存在唯一

计算得对于 $k = 5, 6, 7$ 条件数分别为 $1.5 times 10^7, 4.8 times 10^8, 1.5 times 10^10$
计算得对于 $k = 5, 6, 7$ 条件数分别为 $1.5 times 10^7, 4.8 times 10^8, 1.5 times 10^10$
156 changes: 156 additions & 0 deletions 计算方法B/code/hw6/上机作业.typ
Original file line number Diff line number Diff line change
@@ -0,0 +1,156 @@
#import "../../../template.typ": *
#import "@preview/cetz:0.3.1": *
#import "@preview/cetz-plot:0.1.0": *
#show: note.with(
title: "作业6",
author: "YHTQ",
date: datetime.today().display(),
logo: none,
withOutlined : false,
withTitle : false,
withHeadingNumbering: false
)
#let rough(x) = {
if x == 0{
3
}
else{
1 / (x * x)
}
}
#let laugrange(f, x, xs) = {
let res = 0.0
for xi in xs{
let l = 1
for xj in xs{
if xj != xi{
l *= (x - xj) / (xi - xj)
}
}
res += l * f(xi)
}
res
}
#let divided_difference(f, xs) = {
let n = xs.len()
if n == 1 {
f(xs.at(0))
}
else{
(divided_difference(f, xs.slice(0, -1)) - divided_difference(f, xs.slice(1))) / (xs.first() - xs.last())
}
}
#let Newton(f, x, xs) = {
let n = xs.len()
let res = f(xs.at(0))
for i in range(2, n + 1){
let term = divided_difference(f, xs.slice(0, i))
for j in range(i - 1){
term *= (x - xs.at(j))
}
res += term
}
res
}
#let f_t = (x => x * x + 1)

#let piecewise_linear_base(x0, x1, x2, x) = {
if x0 <= x and x <= x1 and x0 != x1 {
(x - x0) / (x1 - x0)
}
else if x1 <= x and x <= x2 and x1 != x2 {
(x2 - x) / (x2 - x1)
}
else{
0
}
}
#let piecewise_linear(f, x, xs) = {
let n = xs.len()
let res = 0
res += piecewise_linear_base(xs.at(0), xs.at(0), xs.at(1), x) * f(xs.at(0))
for i in range(0, n - 1){
res += piecewise_linear_base(xs.at(i - 1), xs.at(i), xs.at(i + 1), x) * f(xs.at(i))
}
res += piecewise_linear_base(xs.at(n - 2), xs.at(n - 1), xs.at(n - 1), x) * f(xs.at(n - 1))
res
}
#let piecewise_hermit_bases(x0, x1, x) = {
if x0 <= x and x < x1{
(
(1 + 2 * (x - x0) / (x1 - x0)) * calc.pow((x - x1)/(x0 - x1), 2),
(1 + 2 * (x - x1) / (x0 - x1)) * calc.pow((x - x0)/(x1 - x0), 2),
(x - x0) * calc.pow((x - x1)/(x0 - x1), 2),
(x - x1) * calc.pow((x - x0)/(x1 - x0), 2)
)
}
else{
(0, 0, 0, 0)
}
}
#let piecewise_hermit(f, f_d, xs, x) = {
xs.windows(2).map(
x_p => {
let (x0, x1) = x_p
let (a0, a1, b0, b1) = piecewise_hermit_bases(x0, x1, x)
a0 * f(x0) + a1 * f(x1) + b0 * f_d(x0) + b1 * f_d(x1)
}
).sum()
}
#let fd(x) = {2 * x}
#let rough_d(x) = {
if x == 0{
0
}
else{
-2 / (1 + x * x)
}
}
#let xs = range(11).map(x => x - 5)
#let xsl = range(21).map(x => 5 * calc.cos((2 * x + 1) * calc.pi / 42))
本次代码作业直接使用 Typst 完成,源代码就在 `上机作业.typ` 文件之中,代码力求简洁,在性能上还有很大的优化空间。结果如下:(其中 Newton 插值的图像几乎完全和 Lagrange 插值重合,因此难以看到)
#canvas(
{
plot.plot(
size: (13, 10),
// x-tick-step: 0.5,
y-tick-step: 1,
y-min:-2,
y-max: 10,
{
plot.add(
domain:(-5, 5),
(rough),
samples: 100,
label: [Rough 函数],
)
plot.add(
domain: (-5, 5),
(x => Newton(rough, x, xs)),
samples: 1000,
label: [Newton 插值],
)
plot.add(
domain:(-5, 5),
(x => laugrange(rough, x, xs)),
samples: 1000,
label: [Lagrange 插值],
)
plot.add(
domain:(-5, 5),
(x => piecewise_linear(rough, x, xs)),
samples: 50,
label: [分段线性插值],
)
plot.add(
domain:(-5, 5),
(x => piecewise_hermit(rough, rough_d, xs, x)),
samples: 2000,
label: [分段 Hermite 插值],
)
},
)
}
)

可见对于 Rough 函数,任何多项式逼近和分段多项式逼近在 $0$ 附近都不能成功(理论上这是显然的)。同时,Lagrange 插值和 Newton 插值在大部分区间上的表现都相当糟糕,而分段线性和分段 Hermite 插值在稍微远离 $0$ 的区间上表现都相当好。

0 comments on commit e29f154

Please sign in to comment.