diff --git "a/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" "b/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" index e6223f5..2ef0db5 100644 --- "a/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" +++ "b/\346\225\260\347\220\206\351\200\273\350\276\221/main.typ" @@ -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) @@ -98,7 +98,7 @@ - 如果任取变元的所有赋值,该命题形式均为真,则称该命题形式为重言式/永真式 - 如果任取变元的所有赋值,该命题形式均为假,则称该命题形式为矛盾式 - 否则称该命题形式为可满足式 - 判断一个命题形式是否可可满足式是一个 NP 问题,该问题称为 SAT 问题 + 判断一个命题形式是否可可满足式是一个 NP 问题,该问题称为 SAT 问题 ] #definition[][ - 若 $calA -> calB$ 是重言式,则称 $calA$ 蕴含 $calB$,记作 $calA => calB$ @@ -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$ 作为连接符,则称其为受限命题形式 @@ -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$ @@ -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$ @@ -287,7 +287,7 @@ + #indent(2) $calA -> calB := #MPb(4, 1)$ ] ] - + ] #theorem[演绎定理2][ 若 $Gamma tack calA -> calB$,则 $Gamma union {calA} tack calB$ @@ -336,7 +336,7 @@ #definition[重言式][ 若 $v models calA$ 对任意赋值 $v$ 都成立,则称 $calA$ 是重言式,记作 $models calA$ ] - + == 完全性定理 前面的形式系统使用的是证明论的思想,使用 $tack$,是指纯粹语法的推断。而之前的章节从真值指派看待命题逻辑,使用的是模型论的思想,使用 $models$,指通过语义进行的分析。完全性定理即是说,这两种思想是等价的。 #theorem[命题逻辑的可靠性(soundness)][ @@ -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[命题逻辑的一致性][ @@ -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 @@ -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))$ ][ @@ -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 中的公式集和项集都是至多可数的 ] @@ -526,7 +526,7 @@ - 对于谓词符,存在一些对象满足这个谓词,而另一些不满足 - 对于函项符,它将一些对象映射为另一个对象 这应该能准确的描述一阶逻辑中的非逻辑符号的解释。这被称为 FOL 假设。 - + 具体而言,我们可以依赖于集合论建立一阶语言的模型: #definition[Tarski][ 一个一阶语言 $language$ 的解释 $Interpret$ 包括: @@ -549,7 +549,7 @@ 为了方便,假设 $language$ 中的常元为 $a_1, ..., a_i, ...$,我们就可以记: $ - D_I = {a_i} + D_I = {a_i} $ (如果常元不足,做常元扩展即可)\ 该记法成立是因为 $D_I$ 是元语言中的集合,其中元素与记法无关,因此不妨就用 #language 中的常元符号。 @@ -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)$ @@ -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) $ ] @@ -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$][ diff --git "a/\350\256\241\347\256\227\346\226\271\346\263\225B/code/hw6/hw6.typ" "b/\350\256\241\347\256\227\346\226\271\346\263\225B/code/hw6/hw6.typ" index 52cfab2..b1b5280 100644 --- "a/\350\256\241\347\256\227\346\226\271\346\263\225B/code/hw6/hw6.typ" +++ "b/\350\256\241\347\256\227\346\226\271\346\263\225B/code/hw6/hw6.typ" @@ -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 @@ -31,7 +31,7 @@ l *= (x - xj) / (xi - xj) } } - res += l * calc.sin(xi) + res += l * f(xi) } res } @@ -39,18 +39,18 @@ $ 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)$,注意到: $ @@ -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$ \ No newline at end of file + 计算得对于 $k = 5, 6, 7$ 条件数分别为 $1.5 times 10^7, 4.8 times 10^8, 1.5 times 10^10$ diff --git "a/\350\256\241\347\256\227\346\226\271\346\263\225B/code/hw6/\344\270\212\346\234\272\344\275\234\344\270\232.typ" "b/\350\256\241\347\256\227\346\226\271\346\263\225B/code/hw6/\344\270\212\346\234\272\344\275\234\344\270\232.typ" new file mode 100644 index 0000000..cef1955 --- /dev/null +++ "b/\350\256\241\347\256\227\346\226\271\346\263\225B/code/hw6/\344\270\212\346\234\272\344\275\234\344\270\232.typ" @@ -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$ 的区间上表现都相当好。 \ No newline at end of file