贰岛 - TwinIsland
type: channel
link: https://cirno.me/author/1/
description: TwinIsland
items: Intro Program Verification
items: 多伦多寒假游记
items: 音特美+Drop ERX 耳机开箱
items: 傅里叶变换生成频谱图
items: Typecho Void主题美化
items: Rust 速通从0到1
items: Operation System: Reading Log 1
items: Algorithm: 范围查询(Range)
items: CS361: Note for Midterm2
items: CS412: Note for Midterm2

Intro Program Verification
type: item
date: 2024-10-17T19:10:00+00:00
description: IntroductionWhy we use program verification: mathematics can be used to state program properties and to prove a program correct for all inputs.Limitation: We have only limited ways of convincing ourselves that we have given the right specification: there can be mistakes in the specification and in capturing the informal requirements. In addition, all we can prove at best is the correctness of a mathematical abstraction, never of the system running in the real world.Programming Verification Methodsdeclarative program VS imperative programming: a declarative program $P$ in a language based on a given logic is typically a logical theory in that logic. the properties that we want to verify are satisfied by $P$ can be stated in another theory $Q$.Equational TheoriesTheories in equational logic are called equational theories. In Computer Science they are sometimes referred to as algebraic specifications.An equational theory is a pair $(\Sigma, E)$, where:$\Sigma$ called the signature, describes the syntax of the theory, that is, what types of data and what operation symbols (function symbols) are involved;$E$ is a set of equations between expressions (called terms) in the syntax of $\Sigma$the $\Sigma$ can be more or less expressive, depending on how many types (called sorts) of data it allows, relationships between types:unsorted: kind signatures have only one sortmany-sorted: allow different sorts, like Integer, Bool, List...ordered-sorted: allow different sorts, e.g. Natural < Integer < Rational.MaudeIn Maude, functional modules are equation theories $(\Sigma, E)$, declared like:$$ \text{fmod}(\Sigma, E)\text{endfm} $$Such theories can be unsorted, many-sorted, or order-sorted, or even more general membership equational theories.Many-Sorted SignatureA many-sorted signature is just a labeled multigraph $\Sigma = (S, F, G)$, whose nodes are called sorts $S$, whose labels are called function symbols $F$, and whose labeled multiedges $G$ are called the typings of the funct…

多伦多寒假游记
type: item
date: 2024-01-20T05:01:00+00:00
description: 受好基友之邀，今年寒假去多伦多半个月深度游了一趟。因为咱村寒假不长，所以我基本上刚考完final就坐飞机去多伦多了。那天运气额外的好，值机选座位给我安排到了经济舱第一排，空间感觉比头等舱还大。当时走得太仓促结果穿了条起球的裤子，看着跟homeless一样 芝加哥头上就是多伦多，所以飞机没做多久就到了，本来打算在天上给celeste登顶结果一个章节都没打完。下飞机过完海关差不多4点过，坐上兄弟的车就去干饭了。of course，饭后少不了欢乐饮酒环节 因为去了大半个月，所以中途细枝末节的行程安排有点记不太清了，反正每天大概是吃了喝，喝了睡，一天能猛干四顿饭。不得不说大城市就是好，在俺乡下玉米地中餐虽然不少但质量都不太高。还记得大一刚到学校随便去了家中餐厅点了个肝腰合炒，我叼，这肉吃着就跟马桶炸了一样。说回多伦多，因为当地华人多，无论是中餐馆还是华超质量都特别高，一些地方看着还以为回国了。加拿大地广人稀，很多地方都光秃秃的，和我之前以为的大城市纸醉金迷不太一样，更多的是自然风光：当然作为发达城市，多伦多同样有繁华的一面：右图为多伦多地标建筑：CN Tower街道以及唐人街芳文社yyds尼加拉瀑布是由三座位於北美洲五大湖區尼加拉河上瀑布的總稱唐突繁体字，因为俺是从wiki上复制的 ∠( ᐛ 」∠)＿ 。距离加拿大车程1小时左右，虽然有点儿远但绝对不枉此行，因为它实在是太大了！！！这边鸟似乎不怕人（从瀑布回来后也正好快过年了，和哥们儿脑袋一热一起换了新手机结果直接金融危机，本来过年那天打算去下馆子吃点好的，结果只能降级搞了两盒炸鸡以及3L的啤酒+大摩，下次再像这样一起喝酒聊骚不知道得等到多久以后了。新年后加拿大之旅就迎来尾声了，后面几天去了加拿大周边景点，比如多伦多动物园，以及又去了趟downtown把没买的东西给买了。“人生苦短，及时行乐”。对我而言，家人身体健康，平时能和他们一起聊天。身边三五好友，一两知己，有空喝酒撩骚，分享烦心事。身边没逼人，没逼事，对我来说就是最大的“乐”。新的一年反省了一下自己，自己似乎并没有和父母主动聊天，对学业也远不及大一大二那么勤奋。我知道光是反省肯定不够，因此我这学期报了6节课给自己上压力；每周强迫自己至少给父母和爷爷打一次电话，多和家人交流；学会拒绝。

音特美+Drop ERX 耳机开箱
type: item
date: 2023-12-15T23:34:00+00:00
description: 上周看drop官网打折瘾犯了 就入了。先说说快递，drop发的dhl美国境内给我寄了10天 ，后面都快忘了买耳机这事儿 box frontbox back买之前看测评以为包装挺大，但其实一般，如下是包装和fumo大小对比 (ᗜ ˰ ᗜ) suika and iem包装里的配件还算凑合，一包三节套，一包配套，两个绿色调音滤嘴，耳机在收纳盒里现在说说耳机本体，腔体是不锈钢材质拿着很瓷实，代价就是腔体会比较重，差不多和一众多动铁一个重量。p1/p2为默认配套，个人感觉偏大，普通耳套我一般戴L但这个只能M。和er系列一样这个耳机同样得深插，如果没戴好的话声音会变的很糊。默认套我一直戴不好，所以最后配三节套在用。耳机插脑子感觉还挺爽的 对于听感，现在潜听了一下感觉还是不错的。调音中正，对乐器还原以及定位能算得上是我目前听过耳机的top级别。freqency response古典方面适合小编制，独奏，协奏。人声表现还算凑合。试听了两个自己比较常听的几盘专，普罗科菲耶夫钢协对每个乐器的还原堪称一绝，尤其是钢琴华彩，有种在现场听的感觉；普契尼图兰朵里独唱音色非常美，但对大场面的分离度会差些：Prokofiev: Piano Concerto No. 3 / Bartók: Piano Concerto No. 2"Puccini: Turandot再来说说人声，这耳机听男声女声都还行但肯定算不上毒。acg的话分类型，ost很nice但炸的那种就一般了。摇滚我主要听indie，prog，乐器摇滚…这耳机听着都还不错，特别是indie听着有种监听的感觉。Black Midi: HellfireYuru camp S1 OST最后说说缺点，这耳机因为是单动铁所以解析不太行，具体表现就是大编制会有点乱。还有要注意这耳机高阻底敏不太好推，前端一般不建议盲狙（可以先用这耳机兄弟er4xr试试）

傅里叶变换生成频谱图
type: item
date: 2023-11-27T06:54:00+00:00
description: 问题机器学习课上的一道题，题目是：仅使用矩阵乘法来生成频谱图矩阵。输入声音数据是一个列向量 $x$。请详细描述您将如何构建一个矩阵 $A$，使得 $A∙x$ 将产生复数频谱系数的 $vec(∙)$。$\text{DFT_size}=64，\text{Hop_size}=32$，并使用Hann window减少泄漏。As promised in class, matrix multiplies can perform all kinds of linear operations.Here you will have to implement a spectrogram using only a matrix multiplication.Your input sound is a column vector x. Describe exactly how you would constructa matrix A, such that the product A∙x will produce the vec(∙) of the complexspectrogram coefficients. Your transform should have a DFT size of 64, a hop sizeof 32, and will use a Hann window. Make an image plot of the real part of the matrixA and allow me to marvel at its beauty.解答思路要解决这个问题，我们首先假设目标向量（即频谱图）是$S$，输入的声音数据列向量大小为$N$，给定$\text{DFT_size}=64, \text{Hop_size}=32$，帧频的数量就能被表示为：$$ \text{Frame#} = \left\lceil \frac{N - \text{DFT_size}}{\text{Hop_size}} \right\rceil + 1 = \left\lceil \frac{N-64}{32} \right\rceil + 1 $$每个帧频包含 $\text{DFT_size}$ 个频格。这些频格随后构成我们的频谱图向量 $S$。因此，$S$ 的长度可以表示为：$$ |S| = \left\lceil \frac{N-64}{32} \right\rceil \times 64 = 2N - 64 $$根据矩阵乘法的性质，$|S|$ 等于$A$ 中行的数量。所以矩阵 $A$ 的大小应该为 $(2N-64) \times N$现在，让我们确定这个矩阵中每个entry的值。为了计算一个段 $ [a_1, a_2, \ldots, a_{64}]$ 的复数频谱系数，首先应用Hann Window来减少泄漏：$$ w(n) = 0.5 \times \left(1 - \cos\left(\frac{2\pi n}{N-1}\right)\right), \quad N = 64 $$应用Hann Window后的结果数据变为：$$ \text{data_with_hann_window} = \left[ w(1)a_1, w(2)a_2, \ldots, w(64)a_{64} \right] $$随后的步骤是应用 DFT：$$ X(k) = \sum_{n=0}^{N-1} x[n] e^{-j\left(\frac{2\pi kn}{N}\right)} $$给定 $x = \text{data_with_hann_window} $ 以及$N = 64$, 转换过后的数据能表示为：$$ \text{data_with_hann_window_DFT} = \left[ X(0), X(1), \ldots, X(63) \right] $$为了以矩阵形式表示这个过程，并考虑到Hop size，让我们定义三个函数：$$ X(n, k) = e^{-j(2\pi nk/64)} \\ H(k) = 0.5 \times \left(1 - \cos\left(\frac{2\pi k}{63}\right)\right) \\ q(i) = 32 \left( \left\lfloor \frac{i}{64} \right\rfloor \right) $$对于矩阵 $A$，其第 $i$ 行和第 $j$ 列的元素表示为 $A_{i, j}$，该元素必须满足以下条件：Matrix A for sound sample size 64从对$A$的可视化中，我们不难看出矩阵$A$是中心对称的，所以生成算法其实还有优化的空间，但由于只是作业就没…

Typecho Void主题美化
type: item
date: 2023-11-26T03:52:00+00:00
description: 头图跟随鼠标移动其实俺就是薅的b站头图代码 ，实现起来也不复杂，在VOID/includes/banner.php最后那里的<?php elseif($this->is('index')): ?>条件判断中添加一段脚本就行: <?php elseif($this->is('index')): ?> <?php $title = Helper::options()->title; if($setting['indexBannerTitle']!='') $title = $setting['indexBannerTitle']; $subtitle = Helper::options()->description; if($setting['indexBannerSubtitle']!='') $subtitle = $setting['indexBannerSubtitle']; ?> <div class="banner-title index<?php if(!empty($banner)) echo ' force-normal'; ?>"> <?php echo $title; ?> <?php echo $subtitle; ?> <?php endif; ?> 点击头图放大功能在主题css中添加：#scrollButton { position: absolute; left: 50%; bottom: 10px; color: white; transform: translateX(-50%); } #scrollButton:hover { filter: drop-shadow(2px 5px 6px white); } #scrollButton.rotated { transform: rotateX(180deg); /* Rotates the button 180 degrees around the X-axis */ transition: transform 0.5s ease; /* Smooth transition for rotation */ } .lazy-wrap:not(.no-banner) { min-height: 0vh; filter: brightness(1); transition: min-height 0.5s ease, filter 1s ease; }类似跟随鼠标移动效果，在banner.php的<?php elseif ($this->is('index')): ?>块中加入一段代码： <?php if (!Utils::isMobile()): ?> <path id="XMLID_225_" d="M325.607,79.393c-5.857-5.857-15.355-5.858-21.213,0.001l-139.39,139.393L25.607,79.393 c-5.857-5.857-15.355-5.858-21.213,0.001c-5.858,5.858-5.858,15.355,0,21.213l150.004,150c2.813,2.813,6.628,4.393,10.606,4.393 s7.794-1.581,10.606-4.394l149.996-150C331.465,94.749,331.465,85.251,325.607,79.393z" /> <?php endif; ?>如果想让移动端也显示此效果，把最外层的if判断注释掉就ok啦！

Rust 速通从0到1
type: item
date: 2023-11-25T07:34:00+00:00
description: Rust代码高亮还没支持，后面会修复这个问题因为是速通，不能涵盖到语言所有特性，但是保证能写出能跑的代码。详细教程可以看Rust官方出的The Rust Programming Language。阅读建议有一定的C/C++基础，了解 指针，Struct，OOP的基本概念以及用法。边读边写代码。包管理类似于npm, pipenv Rust 用 Cargo 进行包管理，常用指令如下：新建项目：cargo new 运行完后，会在项目文件根目录生成一个TOML文件，用过npm的话应该会很熟悉：[package] name = "ProjectName" version = "0.1.0" edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies]运行项目：cargo new过后会生成src/main.rs，main.rs 是项目的入口文件，里面会初始化自带一个Hello World程序，现在咱尝试运行它cargo build # 编译当然你也能用rustc进行古法编译。具体见文档编译后的binary在./target/debug/ 目录下。如果不想这么麻烦，cargo还提供一个指令能一键运行:cargo run # 直接运行如果你项目已经写完了准备发布，可以用cargo build --release来优化编译，缺点是比普通build慢。Debug:cargo check # 查bug这个指令因为跳过了编译成可执行文件的步骤，所以比cargo run/build快，debug的时候用很合适安装依赖：这里先介绍一个额外的概念crate，crate是 Rust 源代码文件的集合。crate可以是二进制的，也就是一个可执行文件。crate 也可以是一个库（library），其中包含了用于其他程序的代码，不能单独执行（类似 .so, .dll, .h）。比如现在我们要装一个生成随机数的library crate：，咱先编辑Cargo.toml加一个依赖:[dependencies] rand = "0.8.5"然后重新用cargo build重新编译项目，done！更新依赖：更新项目中的所有依赖：cargo update为什么用cargo:对于网上任意一个rust项目，如果你想在本地运行，现在不需要手动装依赖、解决版本冲突...只需要三个命令直接秒了：git clone example.org/someproject cd someproject cargo build基本语法咱写个基本的猜数字游戏（Guessing Game）来快速过一遍基本语法，这个游戏用python写出来长这样：import random magic_number = random.randint(1, 10) while True: guess = input("Your Guess: ") if guess < magic_number: print("too small") elif guess > magic_number: print("too large") else: print("you win") break接下来我们用Rust实现同样的功能，我们先实现获取用户输入：use std::io; fn main() { println!("Guess the number!"); println!("Please input your guess."); let mut guess = String::new(); io::stdin() .read_line(&mut guess) .expect("Failed to read line"); println!("You guessed: {guess}"); }相信大家看到如上代码应该不会特别陌生，但有两个地方需要着重说一下：let mut guess = String::new(); // 定义变量在Rust中，变量初始情况都是immutable的（类似const），如果想定义变量就得像如上一样加个mut关键字。io::stdin() .read_line(&mut guess) .expect("Failed to read line");这段代码通过stdin获取用户输入，并传递给&mut guess这个reference，没错，Rust里的&也表示Reference。错误处理：read_line(&mut guess)的返回值是Result，Result是一个enum = {Ok, Err}，Ok代…

Operation System: Reading Log 1
type: item
date: 2023-11-08T00:47:00+00:00
description: IntroductionHow program run on a computer: it executes instructions. Many millions (and these days, even billions) of times every second, the processor fetches an instruction from memory, decodes it (i.e., figures out which instruction this is), and executes it. After it is done with this instruction, the processor moves on to the next instruction, and so on, and so on, until the program finally completes.To ensure system operate correctly and efficiently in an easy-to-use manner, OS use a general techniques called visualization.Visualization the OS takes a physical resource (such as the processor, or memory, or a disk) and transforms it into a more general, powerful, and easy-to-use virtual form of itself. that is, system calls or standard library.OS is also sometimes known as resource manager because of its dutyvirtualizing CPU: even for a single core CPU, by visualizing the CPU, it can seemingly run infinite task run at oncevirtualizing memory: echo process accesses its own private virtual address spaceConcurrency: Ensure the OS can execute multi task at once without causing error and inaccuracyPersistence: OS use file system for persistence data on disk.Design goalit takes physical resources, such as a CPU, memory, or disk, and virtualizes them. It handles tough and tricky issues related to concurrency. And it stores files persistently, thus making them safe over the long-term.build up abstraction: make the system easier to usehigh performance, minimize the overheadprovide protection between application, isolate processes from one anotherhigh degree of reliabilityother: energy efficient, security, mobility...VirtualizationIntroduction of some basic virtualization OS involvedProcessThe definition of a process, informally, is quite simple: it is a running program.To make a lot process seemly run at the same time, the OS virtualizing the CPU. By running oneprocess, then stopping it and running another, and so forth, the OS can promote the illusion that many virtual…

Algorithm: 范围查询(Range)
type: item
date: 2023-10-27T17:28:00+00:00
description: QuestionTsinghua Online Judge 范围查询(Range)Solution如果brute force硬算的话，相当于每一个组range都需要跑一次循环来看点在不在range中，复杂度为$O(nm)$ (n个point，m个range). 如果优化的话很容易能想到用binary search，具体思路如下：sort所有的points $O(nlog n)$对每一个新range，在points里面binary search range的开头和结尾，相减得到此range里points的个数 $O(log n)$doneTime Complexity$$ O(nlog n) + m\times O(log n) = O(nlog n + mlogn) $$#include <stdio.h> #include <stdlib.h> // Function to compare integers for qsort int compare(const void *a, const void *b) { return (*(int *)a - *(int *)b); } // Function to perform binary search int binary_search(int *arr, int n, int x) { int left = 0, right = n - 1; while (left <= right) { int mid = left + (right - left) / 2; if (arr[mid] <= x) { left = mid + 1; } else { right = mid - 1; } } return left; } int main() { int n, m; scanf("%d %d", &n, &m); int points[n]; for (int i = 0; i < n; ++i) { scanf("%d", &points[i]); } // Sort the points qsort(points, n, sizeof(int), compare); for (int i = 0; i < m; ++i) { int a, b; scanf("%d %d", &a, &b); // Use binary search to find the count of points lying inside [a, b] int count = binary_search(points, n, b) - binary_search(points, n, a - 1); printf("%d\n", count); } return 0; }

CS361: Note for Midterm2
type: item
date: 2023-04-04T21:55:00+00:00
description: Distribution (Continuous)continuous uniform distribution: A continuous random variable whose probability distribution is the uniform distribution is often called a uniform random variable. If we know nothing about a random variable apart from the fact that it has a lower and an upper bound, then a uniform distribution is a natural modeluniform distribution plotuniform distribution contentmean: $\frac{u+l}{2}$variance: $\frac{(u-l)^2}{12}$exponential distribution: We assume that failures form a Poisson process in time; then the time to the next failure is exponentially distributed.exponential distribution plotexponential distribution formulamean: $\frac{1}{\lambda}$variance: $\frac{1}{\lambda ^ 2}$Normal Distributiona probability distribution that is symmetric about the mean, showing that data near the mean are more frequent in occurrence than data far from the meannormal distribution plot$$ p(x)=(\frac{1}{\sqrt{2\pi}\sigma})\text{exp}(\frac{-(x-\mu)^2}{2\sigma^2}) $$mean: $\mu$variance: $\sigma ^2$68% data within $\sigma$, 95% data within $2\sigma$, 99% data within $3\sigma$A continuous random variable is a normal random variable if its probability density function is a normal distribution.another name for normal distribution is Gaussian distributions.central limit theorem (CLT): under some not very worrying technical conditions, the sum of a large number of independent random variables will be very close to normal.standard normal distribution: $$ p(x)=(\frac{1}{\sqrt{2\pi}})\text{exp}(\frac{-x^2}{2}) $$mean: $0$variance: $1$A continuous random variable is a standard normal random variable if its probability density function is a standard normal distribution.Any probability density function that is a standard normal distribution in standard coordinates is a normal distribution.binomial distribution approximation:when $N$ is huge, we can approximate binomial distribution with normal distribution to reduce calculation cost.Assume h follows the binomial distribution wi…

CS412: Note for Midterm2
type: item
date: 2023-03-30T04:15:00+00:00
description: ItemsetItemset: A set of one or more itemsk-itemset: An itemset containing k itemssupport:absolute support: sup{x} occurrences of an itemset Xrelative support: s{x} probability that a transaction contains Xfrequent: An itemset (or a pattern) X is frequent if the support of X is no less than a minsup threshold σsample itemset{Beer, Diaper}: 3/5 (60%) Beer: 3/5 (60%), if σ = 0.3, they are frequentconfident: The conditional probability that a transaction containing X also contains YCompress Patternfind close pattern instead of all patternclose pattern: pattern (itemset) X is closed if X is frequent, and there exists no super-pattern Y כ X, with the same support as XT1: {a1, ..., a50}; T2: {a1, ..., a100}, close pattern: P1: “{a1, ..., a50}: 2”; P2: “{a1, ..., a100}: 1”Closed pattern is a lossless compression of frequent patternsmax pattern: pattern X is a max-pattern if X is frequent and there exists no frequent super-pattern Y כ XT1: {a1, ..., a50}; T2: {a1, ..., a100}, max pattern: P: “{a1, ..., a100}: 1”Max-pattern is a lossy compression, that is it will cause data lossin many application, mining closed-patterns is more desirable than mining max-patternsMining MethodsApriori AlgorithmBFS algorithm to find itemset frequent patterndownward closure: Any subset of a frequent itemset must be frequent, If ANY subset of an itemset S is infrequent, then there is no chance for S to be frequent (use for pruning).Apriori processcandidate generation:joining: the set A, B can only be joined if their first k-1 items are the samepruning: use downward closurepartitioning:partitioning is a way to reduce passes of transaction database scansAny itemset that is potentially frequent in TDB must be frequent in at least one of the partitions of TDB$min_{support}$ in partitioned zone = $min_{support}$ $\times$ events number in this partition zoneonly need to scan the DB twice to find frequent itempartitionFP-GrowthDFS algorithm to find itemset frequent pattern, can use to deal with huge am…