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 function symbols.In the signature terminology, we call $f: s_1...s_n$ typing of $f$ with input sorts $s_1...s_n$ and result sort $s$. For $a: ε → s$, we called $a\in F$ a constant symbol of sort $s$.many-sort multigraph exampleWhen all operations are unary, signature are exactly labeled graph.Problem in many sorted signature: Many-sorted signatures are still too restrictive. The problem is that some operations are partial, and there is no natural way of defining them in just a many-sorted framework.e.g. we have a typing Op first: list -> Natural . We have then the problem to defining the value of first(nil), which is undefined.Solution: A much better solution is to recognize that these functions are partial with the typing just given, but become total on appropriate subsorts NeList < List of nonempty lists.$\star$ Subsorts also allow us to overload operator symbols.Order-Sorted SignatureAn order-sorted signature $\Sigma$ is a triple $\Sigma = ((S, \lt), F, G)$, where $\lt$ is a partial order relation on the set of sorts called subsort inclusion. That is, it is a binary relation on $S$ that is:irreflective: $\neg(x\lt x)$transitive: $x\lt y$ and $y \lt z$ imply $x\lt z$$\star$ Unless specified otherwise, by a signature we will always mean an order-sorted signature.Connect component of Poset:if $s\leq s'$ or $s' \leq s$, then $s\equiv_{\leq} s'$if $s\equiv_{\leq} s'$ and $s' \equiv_{\leq} s'' $, then $s\equiv_{\leq} s''$We call the equivalence classes modulo $\equiv_{\leq}$ the connected components of the poset order $(S, \leq)$equivalence classes examplesubsort overloaded: In a sort module, there are multi functions with different input sort in the same equivalent classad-hoc overloaded: multi functions with different input sort but not in same equivalent classWe can illustrate the order-sorted signature in a similar way like that in many-sort signature, and draw sorts in the same poset as a set of node:order-sorted graph exampleAlgebrasAn (unsorted, many-sorted, or order-sorted) signature $\Sigma$ is just syntax: provides the symbols for a language; Algebras describe what the language talking about and its semantics.$\star$ Function symbols do not mean anything until they are interprets as actual functions.Definition: The unsorted $\Sigma-\text{algebra}$ is a pair $\mathbb{A}=(A, \__\mathbb{A})$, where $A$ is interpretation of s, is a set specifying the data elements in the algebra $\mathbb{A}$. and $\__\mathbb{A}$ is a symbol interpretation function that maps:each constant $a$ to $a_\mathbb{A}\in A$each function symbol $f$ to a function $f_\mathbb{A}$In Maude, the meaning (interpretation) of a Maude functional module is an algebra, denoted $\mathbb{C}_{\Sigma/E}$, and called its canonical term algebra.$$ \mathbb{C}_{\Sigma/E} = (T_\Omega, \__{\mathbb{C}_{\Sigma/E}}) $$where $T_\Omega$ is constructor terms. To define $\__{\mathbb{C}_{\Sigma/E}}$, requires three properties:Unique Termination: Given any-term $t$, the repeated application in any order of the above equations to $t$ as left-to-right simplification rules always terminates with a unique result.Sufficient Completeness: The simplification of any-term $t$ always terminates in a constructor term.These two properties can all be checked automatically via using Maude tools.Many-Sorted Algebrasin many-sorted algebras, $\Sigma=\text{algebra}$ is a pair $\mathbb{A=(A, \__\mathbb{A})}$, where$A$ is a sorted symbol interpretation function, choosing for each sort symbol $s\in S$ a corresponding data set $A_s$ interpreting that sort. If $S=\{s1,...,s_n\}$, then $A$ is a function:$$ A:\{s1,...,s_n\}→ A_{si} \in \{A_{s1},...A_{sn}\} $$We denote the sort interpretation function $A=\{A_s}_{s\in S\}$, called $A$ an S-indexed set.$\__\mathbb{A}$ is the function symbol interpretation functionOrder-Sorted AlgebrasIn the order-sorted signature, an obvious $\Sigma$ Algebra is the term algebra $\mathbb{T}_{\Sigma}$, where the family of data sets $T_\Sigma \{T_\Sigma, s\}_{s\in S}$where ${\__\mathbb{T}}_{\Sigma}$ are defined in inductive way:$a\in s → {a_\mathbb{T}}_{\Sigma} = a \in \mathbb{T}_{\Sigma, s}$for each $f: w→ s$, ${f_\mathbb{T}}_{\Sigma}$ maps tuple $t1,...,tn$ to the expression (term) $f(t1,...,tn)\in \mathbb{T}_{\Sigma,s}$.if $s \lt s'$, then $T_{\Sigma, s} \subseteq T_{\Sigma, s'}$In order-sorted algebras, to define $\__{\mathbb{C}_{\Sigma/E}}$, besides the two properties above, we also need to guarantee:Sort Preservation: for terms in sort $s$, $t!_E \in T_{\Omega, s}$. This property holds automatically in the unsorted and many-sorted cases, but may fail for order-sorted case.Sensible SignatureA sensible signature prevents the ambiguity that arises when terms could have different meanings. In essence, it ensures that if two different interpretations of a term are possible (due to overloading), those interpretations must be related by the sort hierarchy, meaning one is more specific than the other.if the argument sorts of two overloaded versions of $f$ are related by a subsort relation, then the result sorts $s$ and $s'$ must also be related by the same subsort relation.Lemma: if $\Sigma$ is a sensible order-sorted signature, then for any term $t$ in the term algebra $T_{\Sigma}$, if $t$ belongs to both $T_{\Sigma, s}$, $T_{\Sigma, s'}$, it follows that the sorts $s$ and $s'$ are related by the subsort relation, i.e., $s \equiv_\leq s'$Preregular: A sensible order-sorted signature is called preregular iff for each -term $t$ (possibly with variables $X$), the set of sorts$$ Sorts(t)= \{s\in S| t \in T_{\Sigma(X), s\}} $$includes a least element of such set in the poset, called the least sort of $t$ and denoted $ls(t)$. That is:$$ ls(t) \in Sorts(t) ∧ \forall s' \in Sorts(t), \quad ls(t) \leq s' $$KindWe can extend our signature without losing or changing functionality of our original module, we called such extended signature $\Sigma^\square$, we can do it byadding a new sort [s], called a kind, to each connected component [s], with $\forall s' \in [s], [s] \gt s'$lifting each operator f : s1 ... sn -> s, n ≥ 1, to the kind level as: f : [s1] ... [sn] -> [s].Variablesvariables in Maude are in math sense, and we can also reduce the notion of terms with variables to that of terms without variables (ground terms) in an extended signature (add to $\Sigma$ each $x \in X_s$ as a constant $x: ε → s$ where $X=\{X_s\}_{s\in S}$ of sets of variables for different sort).Note that if $\Sigma$ is a sensible signature, then it is trivial to check that $\Sigma(X)$ is also, by construction, a sensible signature.One can likewise prove that if $\Sigma$ is preregular, then $\Sigma(X)$ is also preregular.$\star$ variable in term $t$ denotes by: $var(t)$Substitutionif $\__\theta = X → T_{\Sigma (Y)}$, where $X, Y$ are variables. Such substitution can be expressed recursively by:$x\theta = \theta(x)$$f(t1,...,tn)\theta = f(t_1\theta, ..., t_n\theta)$EquationsAn equational theory is then a pair $(Σ, E)$, with $Σ$ and order-sorted signature, and $E$ a set of $Σ$-equations.SubtermsIn a $\Sigma$-term $f(t1, . . . , tn)$, the $t1, . . . , tn$ are called its immediate subterms, denoted $t_i \lhd f(t1, ..., tn); 1 \leq t \leq n$ . Note that the inverse relation $\lhd^{-1} = \rhd$ is well-founded, i.e., terminating.A term $u$ is called subterm of $t$ iff $t \rhd^* u$, and a proper subterm of $t$ iff $t \rhd^+ u$. Note that the relation $\rhd^+$ is also well-founded and a strict order.To indicate where a subterm $u$ is located we can replace $u$ by a hole $[]$. For example, we can indicate the two places where $g(a)$ occurs in $f (b, h(g(a)), g(a))$ by $f (b, h([]), g(a))$ and $f (b, h(g(a)), [])$. A term with a single occurrence of a hole $[]$ is called a context. We write $C[]$ to denote the context. we can obtain a new term, denoted $C[u]$, by replacing the hole $[]$ by the term $u$.Equational and RewritingEquational deduction is the systematic replacement of equals by equals using the given equations $E$. Algebraic simplification produces a special type of equational proofs, called algebraic simplification proofs, where equations are always applied from left to right. This left to right process is called term rewriting, or term reduction.$\star$ Given a sensible order-sorted signature $Σ = ((S,<), F, G)$, a $Σ$-rewrite rule is a sequent $t → t'$, and where we require that the rule $t → t'$is well-typed, in the sense that there are sorts $s, s' \in S$ such that $t\in T_{\Sigma, s}$, $t'\in T_{\Sigma, s'}$, and $[s] = [s']$.A term rewriting system is then a pair $(Σ, R)$, with $Σ$ an order-sorted signature, and $R$ a set of Σ-rewrite rules.E-equality relation: $↔_E^*$ or $=_E$. It is also called the relation of equality modulo $E$. Problem: However, certain equations are intrinsically problematic for term rewriting, for example, $x+y=y+x$, as 1. we do not obtain a simpler term, but only a “mirror image” of the original term; 2. even worse, we can easily loop when applying this equation. The solution to this problem is to build in certain, commonly occurring equational axioms. Let Σ be a sensible order-sorted signature. A rewrite theory is a triple $(Σ,B, R)$, where $B$ is a set of $Σ$-equations, and $R$ is a set of $Σ$-rewrite rules.$$ u =_B u' → v' =_B v. $$We call $→_{R/B}$ the one-step $R$-rewrite relation modulo $B$, and denote by $→ ^0_{R/B}$. The relation $=_B$, called the 0-step $R$-rewrite relation modulo $B$.An $R$-rewrite proof modulo $B$ is either:a 0-step R-rewrite modulo B of the form $u→ ^0_{R/B}v$, so that. $u=_B v$a sequence of $R$-rewrite steps modulo $B$, in form $v0 →_{R/B} v1 →_{R/B} v2 . . . vn−1 →_{R/B} vn$Sometimes, if we declare our equation not carefully, it may cause the module nonterminating, for example:fmod NAT-SET-NONTERMINATING is protecting NAT . sort NatSet . subsort Nat < NatSet . op mt : -> NatSet [ctor] . op _,_ : NatSet NatSet -> NatSet [ctor assoc comm id: mt] . var X : NatSet . eq X,X = X . endfmIn this case, $ACU$ and idempotency equation together will create a loop, and cause the rewriting never terminating. We can solve it by:restrict idempotency to singleton setsvar N : Nat . eq N,N = N .use subsort overloadingsort NatSet NeNatSet . subsort Nat < NeNatSet < NatSet . op mt : -> NatSet [ctor] . op _,_ : NatSet NatSet -> NatSet [ctor assoc comm id: mt] . op _,_ : NeNatSet NeNatSet -> NeNatSet [ctor assoc comm id: mt] . var X : NeNatSet . eq X,X = X .Executability ConditionsFor every functional module, they should satisfied (1) Unique terminating, (2) Sufficient Completeness, (3) Sort Preservation, and for every constructor term has a canonical term algebra as its sematic.Unique Termination will follow from $\vec E$ being:terminating modulo B, andconfluent modulo BSufficiently Completeness will follow from $\vec E$ being so modulo B, andSort Preservation will follow from $\vec E$ being sort decreasing.$\star$ For each $t→ t' \in \vec E$, any variable $x$ occurring in $t'$ must also occur in $t$, i.e., $vars(t') \in vars(t)$Sort Decreasingness$\star$ (Sort Decreasingness) For each $t→ t'\in \vec E, s \in S$, and each substitution $\theta$, we have $t\theta: s → t'\theta: s$For example, for sorts Nat < Set, with $\cup$ (set union), the rule $x→ x \cup x$, with $x: Set$, is not sort-decreasing, since for the sort specialization $\{x: Set → x': Nat\}$ we have $ls(x')=Nat\lt Set = ls(x'\cup x')$Theorem: $\Sigma$ is $B$-preregular iff the rewrite theory $(\Sigma, \overset {→}{B} \cup \overset {\leftarrow}{B})$ is sort decreasing.$B$-preregular: (1) $\Sigma$ is preregular, and (2) $t=_B t'$ implies that $ls(t)=ls(t')$$\star$ (Determinism/Confluence) if $t$ can be rewrite to both $u, v$. Then, $u =_B v$confluence exampleUnique Terminatingin rewriting theory, rules $\vec E$ are called terminating modulo B iff $→_{\vec E /B}$ is well founded. $\vec E$ is called weakly terminating modulo B has a $\vec E / B$-normal form, i.e., $∃ v \in T, t →_{\vec E/B}v ∧ \not ∃ w \in T \quad s.t. v →_{\vec E/B} w$, denoted as $t →_{\vec E/B}^! v$$\star$ if $\Sigma$ is B-preregular, and $\vec E$ is sort-decreasing, both Unique Termination and Sort Preservation hold.Joinable: two term are joinable if they can be rewrite into the same term.Church-Rosser property:$$ t =_{E\cup B}t' \iff t ↓_{\vec E / b} t' $$Local Confluenceif we have $t →_{R/B}u$ and $t→_{R/B}v$, then $u↓_{R/B}v$.Lemma: a rewrite theory is confluence if it is locally confluent and terminating.we can prove local confluence by proving that all critical pairs are joinable.When we can apply multiple rules to one term, there are three possibilities:Nested Simplification with Overlap: nested simplification with overlap: there is a path $r$ such that $q =p.r$ (or $p = q.r$, but this case is symmetric) and $r$ is a nonvariable position in u; [show all critical pairs are joinable]Nested Simplification without Overlap: nested simplification with overlap: there is a path $r$ such that $q =p.r$ (or $p = q.r$, but this case is symmetric) and r is not a nonvariable position in $u$; [always joinable]Sideways Simplification: there isn’t such an $r$ at all. [always joinable]When we deal with the Nested Simplification with Overlap case, can be reduce to finding, for all pairs of equations $u=v$ and $u'=v'$ in $E$ and all nonvariable positions $p$ in $u$. all solutions to unification problems.Unification:the unification problem consists in, given terms $t$ and $t'$ whose sorts are in the same connected component, finding a substitution $θ$ that makes them equal. finding $\theta$ to make $t\theta = t'\theta$B-Unification: find $\theta$ to make $t\theta =_B t'\theta$Delete: $\frac{\{E\}, t=t}{\{E\}}$Decompose: $\frac{\{E, f(t_1,...,t_n)=f(t_1',...,t_n')\}}{\{E, t_1=t1',...,t_n=t_n'\}}$Conflict: $\frac{\{E, f(t_1,...,t_n)=g(t_1',...,t_m')\}}{\text{failure}}$ if $f \neq g$Coalesce: $\frac{\{E, x=y\}}{\{E\{x→ y\}, x=y\}}$Check: $\frac{\{E, x=t\}}{\text{failure}}$ if $x\in vars(t), x \neq t$Eliminate: $\frac{\{E, x=t\}}{\{E\{x→ t\}, x=t\}}$ if $x\not \in vars(t), t \not\in V, x \in vars(E)$e.g.{f(g(x, h(y)), z) = f(z, g(k(u), v))} −→ (Decompose) {g(x, h(y)) = z, z = g(k(u), v)} −→ (Eliminate) {g(x, h(y)) = g(k(u), v), z = g(k(u), v)} −→ (Decompose) {x = k(u), v = h(y), z = g(k(u), v)} −→ (Eliminate) {x = k(u), v = h(y), z = g(k(u), h(y))}For B-unification, there can be several solutions to a unification problem. Also, we define failure as an identity element for $\_∧\_$e.g.{f(g(h(y), x), z) = f(z, g(k(u), v))} −→ (Decompose) {g(h(y), x) = z, z = g(k(u), v)} −→ (Eliminate) {g(h(y), x) = g(k(u), v), z = g(k(u), v)} −→ (Decompose-C) {x = v, k(u) = h(y), z = g(k(u), v)} ∨ {x = k(u), v = h(y), z = g(k(u), v)} −→ (Conflict ∨ Eliminate) failure ∨ {x = k(u), v = h(y), z = g(k(u), h(y))} = {x = k(u), v = h(y), z = g(k(u), h(y))} applying the resulting unifier we obtain the identity, f(g(h(y), k(u)), g(h(y), k(u))) =comm f(g(k(u), h(y)), g(k(u), h(y))).Critical Pairse.g.Notice that none of the equation in the module share the same variable, our rule set for this module will simply be convert all equation to be oriented:$$ \vec{E} = \{x+0 → x, y+s(z) → s(y+z), (x1+y1)+z1→ x1+(y1+z1)\} $$To compute the set of all critical pairs of this module, we need to find:$$ CP(\Sigma, \vec{E}) = \left( \bigcup_{1 \leq i < j \leq n} CP(u_i \to v_i, u_j \to v_j) \cup CP(u_j \to v_j, u_i \to v_i) \right) \cup \bigcup_{1 \leq i \leq n} CP(u_i \to v_i, u'_i \to v'_i) $$where $\vec{E} = \{ u_1 \to v_1, \dots, u_n \to v_n \}$. We can calculate all critical pairs $CP(u→ v, w → q)$:Calculate: $CP(y+s(z) → s(y+z), x+0 → x)$In this case, $p=\{ε, 2\}$, and when $p=ε$:$$ \theta \in Unif_{\Sigma}(y+s(z) = x+0) $$However, the unification failed since $s(z)$ cannot be unified to be a constant $0$. when $p=2$:$$ \theta \in Unif_{\Sigma}(s(z) = x+0)= \{s(z)→ x+0\} $$it cannot be unified because $top(x+0)=+ \neq s = top(s(z))$ (Remark 1)TerminationA well-founded ordering $>$ on $T_\Sigma$ is called a reduction ordering iff it satisfies the following two conditions:strict $\Sigma$-monotonicity: for each $f \in \Sigma$, whenever $f(t_1, \dots, t_n)$, $f(t_1, \dots, t_{i-1}, t'_i, t_{i+1}, \dots, t_n) \in T_\Sigma(V)$ with$t_i > t'_i$, then $f(t_1, \dots, t_n) > f(t_1, \dots, t_{i-1}, t'_i, t_{i+1}, \dots, t_n)$.closure under substitution: if $t > t'$, then, for any substitution $\theta : V \to T_\Sigma(V)$ we have $t\theta > t'\theta$.Theorem: For any equational theory, $\vec E$ is terminating iff there exists a reduction order $\gt$ s.t. $\forall (u=v)\in E, u \gt v$RPO:The recursive path ordering (RPO) is based on the idea of giving an ordering on the function symbols in Σ, which is then extended to a reduction ordering on all terms.Given a finite signature $\Sigma = ((S, <), F, G)$, plus an ordering $>$ and a status function $\tau$ on its symbols $F$, the recursive path ordering $>_{\text{rpo}}$ on $\bigcup_{s \in S} T_\Sigma(V)$ is defined recursively as follows. $u >_{\text{rpo}} t$ iff: $u = f(u_1, \dots, u_n)$, and either:$u_i \geq_{\text{rpo}} t$ for some $1 \leq i \leq n$, or$t = g(t_1, \dots, t_m)$, $u >_{\text{rpo}} t_j$ for all $1 \leq j \leq m$, and either:$f > g$, or$f = g$ and $\langle u_1, \dots, u_n \rangle >^{\tau(f)}_{rpo} \langle t_1, \dots, t_n \rangle$f $f$ has $n$ arguments and $\tau(f) = \text{lex}(\pi)$ with $\pi$ a permutation on $n$ elements, then $\langle u_1, \dots, u_n \rangle >_{\tau(f)}^{\text{rpo}} \langle t_1, \dots, t_n \rangle$ iff there exists $i$, $1 \leq i \leq n$ such that for $j < i$, $u_{\pi(j)} = t_{\pi(j)}$, and $u_{\pi(i)} > t_{\pi(i)}$.If $\tau(f) = \text{mult}$, then $\langle u_1, \dots, u_n \rangle >_{\tau(f)}^{\text{rpo}} \langle t_1, \dots, t_n \rangle$ iff we have $\{u_1, \dots, u_n\} >_{\text{mult}}^{\text{rpo}} \{t_1, \dots, t_n\}$.$\star$ we need a reduction order that is compatible with the axioms $B$. That is, if $u > t, u =_B u_0$ and $t =_B t_0$ , then we must also have $u_0 > t_0$Polynomial Orderings:Another general method of defining suitable reduction orderings is based on polynomial orderings. In its simplest form we can just use polynomials on several variables whose coefficients are natural numberswe assign each function symbol in $\Sigma$ a polynomial $pf$ involving exactly the variables $x_1, ..., x_n$. If $f$ is subsort overloading, we assign the same $pf$ to all such overloadings. Also, each constant symbol $b$ associate a positive number $p_b \in \mathbb{N}$. We assign variable to itself $p_x = x$e.g.f(g(x)) = g(f(x))$p_f = x_1 ^3$$p_g=2x_1$$p_a = 3$We can prove that $((2x)^3)_{\mathbb{N}\geq k} \gt (2(x^3))_{\mathbb{N}\geq k}$, hence terminating.Sufficient Completenesseach $u\in T_\Sigma \quad \text{s.t.}\quad t→^!_{\vec E/B}u$, we have $u\in T_\Omega$.$\star$ if the kind-completed signature $\Sigma^\square$ is kind-complete, then the requirement for sufficient completeness should apply only to terms in the original signature $\Sigma$, not in the kind-completed signature $\Sigma^\square$.Free modulo: the constructors are free modulo $B$ if the following condition holds: For each term $u$ of sort $s$ (where $s$ is not a kind) built from constructors (terms in $T_\Omega$), the term $u$ is already in its normal form with respect to the equations in $B$ and the rewrite rules $→_E$.Check Sufficient CompletenessFor arbitrary equational theories sufficient completeness is in general undecidable. However, in practice, For equational theories satisfying the above requirements(i) left-linear (i.e., there are no repeated variables in the lefthand side term of the equation); (ii) sort-decreasing; and (iii) terminating.we can use decidability results from tree automata theory to cast the sufficient completeness problem into a tree automata problem and decide the problem that way.we can use decidability results from tree automata theory to cast the sufficient completeness problem into a tree automata problem and decide the problem that way.Automata: An ordinary finite-state automaton $A$ has a finite set $Q$ of states and accepts strings of inputs when they lead the automaton to a subset $Q_0 ⊆ Q$ of accepting states. The language $L(A)$ of the automaton is then the set of all strings accepted by $A$. Such languages are called regular languages and have nice decidablity results: they are closed under Boolean operations (we can construct automata for each such operation); and we can decide whether $L(A)$ is empty.Tree automata: All this is generalized by finite-state tree automata, which accept terms in an unsorted term algebra $T_\Sigma$ instead of just strings. A tree automaton (TA) is a tuple $A = (\Sigma, Q, Q_0, R)$ with $Σ$ an unsorted signature, $Q$ a set of extra constants not in $Σ$ called states, $Q_0 ⊆Q$ a subset of accepting states, and $R$ a set of transition rules, which can be of two forms:$f(q1, . . . , qn) → q$, with $q1, . . . , qn, q ∈ Q, f ∈ Σ$ and $f(q1, . . . , qn) ∈ T_{Σ(Q)}$ (for n = 0, $f$ will be a constant, and the rule becomes $f → q$)$q → q ′$ , with $q, q′ ∈ Q$; these are called epsilon transitions and define a rule subset $Rϵ ⊆ R$.We then define the language $L(A)$ as the subset $L(A) ⊆ T_Σ$ of those $t ∈ T_Σ$ such that there is a $q ∈ Q_0$ such that $ t →_R^* q$. A subset $L ⊆ T_Σ$ is called regular iff there is a finite-state tree automaton $A$ such that $L = L(A)$.$\star$ Automata are labeled graphs. Tree automata are just labeled multigraphs, actually, order-sorted signaturesUnder conditions (i)–(iii) $(Σ, E ∪ B)$ is sufficiently complete iff for each sort $s$ we have $D_s \ (Red ∪ C_s ) = ∅$, which can be decided by deciding emptiness of the corresponding tree automaton.$D_s$: terms of sort $s$ having a defined symbol on top and constructor terms as arguments$C_s$: constructor terms of sort $s$$Red$: terms reducible by the oriented equations $\vec E$ modulo $B$e.g.To see how the desired tree automata needed to decide sufficient completeness can be built, we can use a simple example, our usual unsorted specification for addition for the Peano natural numbers with a single sort N at, with 0 and s as constructors, and with equations x + 0 = x and x + s(y) = s(x + y). This specification satisfies conditions (i)–(iii), since it is left-linear, confluent, sort-decreasing, and terminating. To recognize each of the regular sets Red, DNat, and CNat we need three tree automata ARed, ADNat , and ACNat .The tree automata ARed, ADNat and ACtor have the same signature Σ (that of the natural numbers), set of states Q = {N at, Red, DNat, Ctor , Zero, NzCtor}, and transitions R:(ϵ-transitions): Ctor → N at, Red → DNat, DNat → N at, Zero → Ctor , NzCtor → Ctor(Nat transitions) s(N at) → N at, N at + N at → N at.(constructor transitions): 0 → Zero, s(Ctor ) → NzCtor .(defined function transition): Ctor + Ctor → DNat.(reducibility transitions): Ctor + Zero → Red, Ctor + NzCtor → RedARed, ADNat and ACtor only differ in their respective accepting state: Red, DNat, and Ctor . Since their: (i) signature, (ii) set of states and (iii) transitions are the same, the shared part (i)–(iii) is exactly the same thing as the order sorted signature:sorts Nat Red, D-Nat Ctor Zero NzCtor . subsorts Zero NzCtor < Ctor < Nat . subsorts Red < D-Nat < Nat . op s : Nat -> Nat . op s : Ctor -> NzCtor . op 0 : -> Zero . op _+_ : Nat Nat -> Nat . op _+_ : Ctor Ctor -> D-Nat . op _+_ : Ctor Zero -> Red . op _+_ : Ctor NzCtor -> Red .The point now is that each Boolean operation on regular tree languages has a corresponding operation on their associated tree automata. Therefore, out of the automata ARed, ADNat , and ACtor we can construct an automaton that recognizes the language DNat \ (Red ∪ Ctor ). Let us call this automaton ADNat(Red∪Ctor) . We know that under conditions (i)–(iii) our specification is sufficiently complete iff DNat \ (Red ∪ Ctor ) = ∅. Therefore, we can decide this property by testing ADNat(Red∪Ctor) for emptiness. If the test (as for this example) succeeds, we are done. If it doesn’t, we get a very useful counterexample term, showing us where sufficient completeness fails.
受好基友之邀，今年寒假去多伦多半个月深度游了一趟。因为咱村寒假不长，所以我基本上刚考完final就坐飞机去多伦多了。那天运气额外的好，值机选座位给我安排到了经济舱第一排，空间感觉比头等舱还大。当时走得太仓促结果穿了条起球的裤子，看着跟homeless一样 芝加哥头上就是多伦多，所以飞机没做多久就到了，本来打算在天上给celeste登顶结果一个章节都没打完。下飞机过完海关差不多4点过，坐上兄弟的车就去干饭了。of course，饭后少不了欢乐饮酒环节 因为去了大半个月，所以中途细枝末节的行程安排有点记不太清了，反正每天大概是吃了喝，喝了睡，一天能猛干四顿饭。不得不说大城市就是好，在俺乡下玉米地中餐虽然不少但质量都不太高。还记得大一刚到学校随便去了家中餐厅点了个肝腰合炒，我叼，这肉吃着就跟马桶炸了一样。说回多伦多，因为当地华人多，无论是中餐馆还是华超质量都特别高，一些地方看着还以为回国了。加拿大地广人稀，很多地方都光秃秃的，和我之前以为的大城市纸醉金迷不太一样，更多的是自然风光：当然作为发达城市，多伦多同样有繁华的一面：右图为多伦多地标建筑：CN Tower街道以及唐人街芳文社yyds尼加拉瀑布是由三座位於北美洲五大湖區尼加拉河上瀑布的總稱唐突繁体字，因为俺是从wiki上复制的 ∠( ᐛ 」∠)＿ 。距离加拿大车程1小时左右，虽然有点儿远但绝对不枉此行，因为它实在是太大了！！！这边鸟似乎不怕人（从瀑布回来后也正好快过年了，和哥们儿脑袋一热一起换了新手机结果直接金融危机，本来过年那天打算去下馆子吃点好的，结果只能降级搞了两盒炸鸡以及3L的啤酒+大摩，下次再像这样一起喝酒聊骚不知道得等到多久以后了。新年后加拿大之旅就迎来尾声了，后面几天去了加拿大周边景点，比如多伦多动物园，以及又去了趟downtown把没买的东西给买了。“人生苦短，及时行乐”。对我而言，家人身体健康，平时能和他们一起聊天。身边三五好友，一两知己，有空喝酒撩骚，分享烦心事。身边没逼人，没逼事，对我来说就是最大的“乐”。新的一年反省了一下自己，自己似乎并没有和父母主动聊天，对学业也远不及大一大二那么勤奋。我知道光是反省肯定不够，因此我这学期报了6节课给自己上压力；每周强迫自己至少给父母和爷爷打一次电话，多和家人交流；学会拒绝。
上周看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试试）
问题机器学习课上的一道题，题目是：仅使用矩阵乘法来生成频谱图矩阵。输入声音数据是一个列向量 $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$是中心对称的，所以生成算法其实还有优化的空间，但由于只是作业就没管那么多了。Codeimport tqdm import matplotlib.pyplot as plt import numpy as np from pydub import AudioSegment sample_size = 20000 DFT_size = 128 Hop_size = 64 DRAW_A = False DRAW_SPECTROGRAM = True SAMPLE_FILENAME = 'sample.m4a' assert (DFT_size / 2 == Hop_size) # DFT function def dft(n, k): return np.exp(-1j * (2 * np.pi * n * k / DFT_size)) # Hann window function def hann(k): return 0.5 * (1 - np.cos(2 * np.pi * k / (DFT_size - 1))) # down sampling, or computer will bomb sample_raw = AudioSegment.from_file(SAMPLE_FILENAME).set_frame_rate(8000) sample = np.array(sample_raw.get_array_of_samples()) N = min(sample_size, sample.shape[0]) sample = sample[:min(sample_size, N)] print(f"sound has shape: {sample.shape[0]}, we use {N} datas as sample") A = np.zeros((2 * N - DFT_size, N)) for i, row in enumerate(tqdm.tqdm(A)): q = Hop_size * (i // DFT_size) for j in range(row.shape[0]): if (j >= q) and (j <= (q + DFT_size)): # A_ij != 0 row[j] = dft(n=j - q, k=i % DFT_size) * hann(j - q) # otherwise A_ij = 0 # visualize A if DRAW_A: plt.imshow(A.real) plt.colorbar() plt.title(f"matrix A (sample size: {sample_size})") plt.axis('off') plt.show() # draw spectrogram if DRAW_SPECTROGRAM: spec_coefficient = A @ sample # keep partial of spec coefficient which can be | 64, add up real and imaginary part, and normalize log10 spec_coefficient = np.abs(spec_coefficient[:spec_coefficient.shape[0] // DFT_size * DFT_size]) spec_coefficient = spec_coefficient.reshape((DFT_size, -1)) plt.imshow(np.log10(spec_coefficient), origin='lower', aspect='auto') plt.colorbar(label='Log Magnitude') plt.title(f"Spectrogram (DFT size: {DFT_size})") plt.xlabel('time frame') plt.ylabel('frequency bin') plt.show()完整版附件附件名称：CS545 HW1.zip文件大小：1097.4 KB下载次数: 455最后修改: 2023-11-27 01:06点击下载
头图跟随鼠标移动其实俺就是薅的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代码高亮还没支持，后面会修复这个问题因为是速通，不能涵盖到语言所有特性，但是保证能写出能跑的代码。详细教程可以看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代表指令成功执行，Err表示出错。除此之外Result里还有一个方法expect，如果 Result 的这个实例是 Ok，expect 将获取 Ok 所保存的返回值并将该值返回给您。在本例中，该值是用户输入中的字节数；如果是Err，程序就会crash然后打印你给expect(msg)方法传的信息。println!类似于printf，支持如下语法：let x = 5; let y = 10; println!("x = {x} and y + 2 = {}", y + 2);现在咱的猜谜游戏能接收用户输入了，下一步生成magic number：let secret_number = rand::thread_rng().gen_range(1..=100);gen_range 方法接受一个范围表达式（range expression）作为参数，并生成在该范围内的随机数。这里使用的范围表达式类型采用了 start..=end 的形式，包含了下界和上界，因此我们需要指定 1..=100 来请求一个介于 1 和 100 之间的数字。use rand::Rng; use std::cmp::Ordering; use std::io; fn main() { // --snip-- println!("You guessed: {guess}"); match guess.cmp(&secret_number) { Ordering::Less => println!("Too small!"), Ordering::Greater => println!("Too big!"), Ordering::Equal => println!("You win!"), } }这段代码虽然看着陌生，但其实很好理解。guess.cmp(&secret_number)比较guess和secret_number并返回enum Ordering。match 类似其他语言的switch，block内讨论三个不同case。现在感觉都没毛病了，但是如果run代码的话会报错。22 | match guess.cmp(&secret_number) { | --- ^^^^^^^^^^^^^^ expected struct `String`, found integer | | | arguments to this function are incorrect 从如上报错信息可以看出是数据类型对不上的原因。Rust是一个强类型语言，guess是String，而secret_number是i32既是int32，所以不能放在一起比大小，正确做法是用parse给guess进行类型转换let guess: u32 = guess.trim().parse().expect("Please type a number!");字符串上的 parse 方法能将一个字符串转换为另一种类型。在这里，我们使用它将一个字符串转换为一个数字类型（因为let guess: u32这里指定了类型）。现在一个基本的猜数字游戏已经做好了，为了能让玩家能够多次尝试，我们还得写个for循环 // --snip-- println!("The secret number is: {secret_number}"); loop { println!("Please input your guess."); // --snip-- match guess.cmp(&secret_number) { Ordering::Less => println!("Too small!"), Ordering::Greater => println!("Too big!"), Ordering::Equal => println!("You win!"), } } }到这里程序就写完了！接下来开始优化程序，比如处理异常输入： // --snip-- io::stdin() .read_line(&mut guess) .expect("Failed to read line"); let guess: u32 = match guess.trim().parse() { Ok(num) => num, Err(_) => continue, }; println!("You guessed: {guess}"); // --snip--其中Ok(num)/Err(_)类似于解包操作，获取enum里面带的message，Err(_)的_和Python一样，代表这个解包的数据不重要。最终程序use rand::Rng; use std::cmp::Ordering; use std::io; fn main() { println!("Guess the number!"); let secret_number = rand::thread_rng().gen_range(1..=100); loop { println!("Please input your guess."); let mut guess = String::new(); io::stdin() .read_line(&mut guess) .expect("Failed to read line"); let guess: u32 = match guess.trim().parse() { Ok(num) => num, Err(_) => continue, }; println!("You guessed: {guess}"); match guess.cmp(&secret_number) { Ordering::Less => println!("Too small!"), Ordering::Greater => println!("Too big!"), Ordering::Equal => { println!("You win!"); break; } } } }Ownership说到Rust，大家想到的第一个词应该改是safety，但为啥它很安全呢，原因就是因为它Ownership概念引入，先来看定义：Ownership is a set of rules that govern how a Rust program manages memoryOwnership 是一系列用于Rust做内存管理的规则在C里面，我们用malloc/calloc/realloc等命令声明内存，当内存不在被使用时，我们需要手动free掉。如果不free就会内存溢出。同样在管理heap上的数据结构（比如实现一个linklist)，稍有不注意就会segfault... 为了解决这个问题，Rust引入了Ownership这个概念，让内存错误不再是个问题。References and Borrowing先来看代码：fn main() { let s1 = String::from("hello"); let len = calculate_length(&s1); println!("The length of '{}' is {}.", s1, len); } fn calculate_length(s: &String) -> usize { s.len() }没错，这段代码和C/C++很像，用&s1表示变量s1的reference。在Rust里，每当你给方法传递参数，参数就属于（owned by）这个方法了，当方法运行结束后就会自动把这个参数drop掉。所以如果你这么写的话：let s1 = String::from("hello"); let len = calculate_length(s1); println!("{s1}"); fn calculate_length(s: String) { // do something }程序就会报错，为什么呢，因为let len = calculate_length(s1)已经把s1的ownership给了calculate_length这个方法，当这个方法运行结束后，s1就会被自动回收，这个时候如果再println!("{s1}")就会找不到s1这个变量。让我们回到最开始的代码，如果我们用reference的话calculate_length(&s1);就会没上述问题，因为Rust管这叫借（borrow），当方法去借一个变量的话就不会take ownership了。是reference，但又不完全是：不同于C，Rust里：传入方法的reference在普通情况下不能被方法修改，比如如下代码就会报错：fn main() { let s = String::from("hello"); change(&s); } fn change(some_string: &String) { some_string.push_str(", world"); }为什么说是在普通情况下呢，因为就像变量能被定义为mut，reference也可以被定义为可变的：fn main() { let mut s = String::from("hello"); change(&mut s); } fn change(some_string: &mut String) { some_string.push_str(", world"); }在上述代码中，我们除了把s变成mut，还把reference也变成&mut s。这个时候传入change就能更改s的值了。mut reference的限制：对于mutable reference，Rust对其有一个限制：对于一个变量，如果你已经有一个关于它的mut reference，在同一个作用域（scope）里就不能再有第二个了，比如如下代码就违反了这个限制，代码会报错：let mut s = String::from("hello"); let r1 = &mut s; let r2 = &mut s; println!("{}, {}", r1, r2);Rust之所以这么设计是为了能在如下情况避免Data Race：两个或更多指针同时访问相同的数据至少有一个指针正在用于写入数据。没有使用机制来同步对数据的访问。上文说到： 同一个scope里就不能再有第二个了...，那如果不在同一个scope还能能定义多个mut reference吗，答案是肯定的：// 不会报错 let mut s = String::from("hello"); { let r1 = &mut s; } // 在这里，r1的作用域结束了，因此我们可以创建一个新的引用。 let r2 = &mut s;Rust同样也不允许统一变量的mut reference和immut reference同时出现，比如如下代码会报错：let mut s = String::from("hello"); let r1 = &s; // OK let r2 = &s; // OK let r3 = &mut s; // 寄！ println!("{}, {}, and {}", r1, r2, r3);如果把上述代码改一下，代码还会报错吗？let mut s = String::from("hello"); let r1 = &s; let r2 = &s; println!("{} and {}", r1, r2); let r3 = &mut s; println!("{}", r3);答案是不会的！为啥呢，因为编译器发现在执行完println!("{} and {}", r1, r2);后r1, r2就再没出现过，所以它就能足够聪明得把r1, r2 在这行过后drop掉。最后跑到let r3这行的时候r1,r2已经影响不到r3啦。ownership转移：当方法返回的变量最后return出去的话，这个变量的ownership就会转移到call它的地方。fn no_dangle() -> String { let s = String::from("hello"); s } fn main() { let result = no_dangle(); println!("{}", result); }Slice现在你准备写一个功能：给一个string，需要返回这个string的第一个单词，你可以这么写：fn main() { let mut s = String::from("hello world"); let word = first_word(&s); // word = 5 } fn first_word(s: &String) -> usize { let bytes = s.as_bytes(); for (i, &item) in bytes.iter().enumerate() { if item == b' ' { return i; } } s.len() }看着没毛病，但有个小问题，如果你后面对s进行了修改，之前定义的word就会失去意义fn main() { let mut s = String::from("hello world"); let word = first_word(&s); s.clear(); // 清空s // 靠，word还是等于5 }如果是写小项目的话这样的问题还很容易发现，但如果是大项目的话就说不准了。这个时候用Rust的Slice结构就能很好的解决这个问题：fn main() { let mut s = String::from("hello world"); let word = first_word(&s); println!("the first word is: {}", word); } fn first_word(s: &String) -> &str { let bytes = s.as_bytes(); for (i, &item) in bytes.iter().enumerate() { if item == b' ' { return &s[0..i]; } } &s[..] }这么写的话word就会从一个赋值过后永远不会变的量变成了reference，也就是说能实时根据s变化而变化了。现在问题又来了，如果在main最后call s.clear()会怎样？fn main() { let mut s = String::from("hello world"); let word = first_word(&s); word.clear(); println!("the first word is: {}", word); }答案是会报错，因为clear()这个方法的实现需要用到word的mut reference，然而之前已经定义了word这个immutable reference。其他类型的Slice：let a = [1, 2, 3, 4, 5]; let slice = &a[1..3]; assert_eq!(slice, &[2, 3]);Struct像很多语言，Rust也有定义Structstruct User { active: bool, username: String, email: String, sign_in_count: u64, } fn main() { // 必须是mutable，Rust不允许只指定部分元素为mutable let mut user1 = User { active: true, username: String::from("someusername123"), email: String::from("someone@example.com"), sign_in_count: 1, }; } fn build_user(email: String, username: String) -> User { User { active: true, username: username, email: email, sign_in_count: 1, } }在build_user里面，因为 username, email 的parameter name和field name一样，所以方法可以简写成：fn build_user(email: String, username: String) -> User { User { active: true, username, email, sign_in_count: 1, } }类似JavaScript, Rust也支持解包操作，比如如上代码你已经定义了一个user1，如果还想定义user2且user2只有email字段和user1.email不一样的话就能简写成：fn main() { // --snip-- let user2 = User { email: String::from("another@example.com"), ..user1 }; }Tuple Struct:比如你想用C实现对一个Pixel的定义，可能会这么写：struct Color { int32_t r; int32_t g; int32_t b; };但其实r,g,b压根儿没必要定义出来，因为大伙都知道Pixel是由这个三个元素组成的，这个时候你就能用到Rust的Tuple Struct来简写这样的数据结构了：struct Color(i32, i32, i32); struct Point(i32, i32, i32); fn main() { let black = Color(0, 0, 0); let origin = Point(0, 0, 0); }Unit-Like Structstruct AlwaysEqual; fn main() { let subject = AlwaysEqual; }Debug:如果我们想打印struct用于Debug的话（不只是struct能用），Rust提供了一个接口能很容易的实现：#[derive(Debug)] struct Rectangle { width: u32, height: u32, } fn main() { let rect1 = Rectangle { width: 30, height: 50, }; println!("rect1 is {:?}", rect1); }你也能用一个更吊的macro：dgb!()，和print不同，dgb能获取调试内容的ownership进而支持用户能写出width: dbg!(30 * scale)的代码，区别2是dgb的调试信息会写到stderr而不是stdout。#[derive(Debug)] struct Rectangle { width: u32, height: u32, } fn main() { let scale = 2; let rect1 = Rectangle { width: dbg!(30 * scale), height: 50, }; dbg!(&rect1); }Method：和很多新语言一样，Rust支持给Struct定义方法（Method），这里我们先回顾一下方法和函数的区别方法 (Method):"方法"通常用于面向对象编程（例如Java、C++等），它是与特定对象或类相关联的功能。方法是一种操作，可以在对象上执行，通常可以访问该对象的属性或状态，并且通常与对象的行为相关。方法是面向对象编程中的一部分，它们是类的成员，因此它们可以通过类的实例来调用。函数 (Function):"函数"是一段独立的可执行代码，通常不与特定对象或类相关联。函数可以独立存在，接受输入参数（如果需要）并返回一个结果。函数可以在程序中的任何地方被调用，而不需要依赖于特定的对象。函数是通用的编程概念，可以在不同编程范式（如面向对象、过程式编程等）中使用。#[derive(Debug)] struct Rectangle { width: u32, height: u32, } impl Rectangle { fn area(&self) -> u32 { self.width * self.height } } fn main() { let rect1 = Rectangle { width: 30, height: 50, }; println!( "The area of the rectangle is {} square pixels.", rect1.area() ); }看到这儿，大家可能会对self.width * self.height产生疑惑，为啥指针不用->而是直接.呢。得益于Rust的automatic referencing and dereferencing 特性，编译器能自动处理转换reference符号。也就是说如下两行是一样的：p1.distance(&p2); (&p1).distance(&p2);关联函数（Associated Function）:有些时候方法的实现并不需要self参数（既 square(&self, size: u32)）类似静态方法，你能这么写：impl Rectangle { fn square(size: u32) -> Self { Self { width: size, height: size, } } }impl其他用法：如下写法都是OK的：impl Rectangle { fn area(&self) -> u32 { self.width * self.height } } impl Rectangle { fn can_hold(&self, other: &Rectangle) -> bool { self.width > other.width && self.height > other.height } } impl Rectangle { fn area(&self) -> u32 { self.width * self.height } fn can_hold(&self, other: &Rectangle) -> bool { self.width > other.width && self.height > other.height } }EnumRust的枚举类型写法是这样的：enum IpAddrKind { V4, V6, } struct IpAddr { kind: IpAddrKind, address: String, } let home = IpAddr { kind: IpAddrKind::V4, address: String::from("127.0.0.1"), }; let loopback = IpAddr { kind: IpAddrKind::V6, address: String::from("::1"), };当然如上是常规写法，Rust的enum支持你给里面的元素定义不同的数据类型以及赋值：enum Message { Quit, // 普通enum元素 Move { x: i32, y: i32 }, // name filed Write(String), // 字符串类型 ChangeColor(i32, i32, i32), // 三个类型 } fn main() { let quit_message = Message::Quit; let move_message = Message::Move { x: 10, y: 20 }; let write_message = Message::Write(String::from("Hello, Rust!")); let color_message = Message::ChangeColor(255, 0, 0); }除此之外你还可以将各种类型的数据放入枚举的变体中，例如字符串、数值类型或结构体。甚至可以包含另一个枚举！可选参数Option：在Rust标准库中，Optional定义为一个枚举类型：enum Option<T> { None, Some(T), }类似于C++的泛型，下一篇文章会介绍使用方法和其他enum一样：let some_number = Some(5); let some_char = Some('e'); let absent_number: Option<i32> = None;这么定义有什么用呢，比如你现在这么写代码就会报错：let x: i8 = 5; let y: Option<i8> = Some(5); let sum = x + y;原因是因为y之前被定义为一个Optional的数据，如果在let sum = x + y; 之前y没被定义那不是寄了，所以Rust如此考量是为了安全。Enum和Match一起使用：fn plus_one(x: Option<i32>) -> Option<i32> { match x { None => None, Some(i) => Some(i + 1), } } let five = Some(5); let six = plus_one(five); let none = plus_one(None);上述写法是完全OK的但是不优雅，因为None => None完全没必要写出来，Optional这个enum只有两个field还好，如果enum贼大，但你又只想math其中一小部分就难搞了。所以Rust提供了 Catch-all 的语法（其实就是default）：let dice_roll = 9; match dice_roll { 3 => add_fancy_hat(), 7 => remove_fancy_hat(), _ => reroll(), // Catch All } fn add_fancy_hat() {} fn remove_fancy_hat() {} fn reroll() {}在Rust里面，Match必须讨论到所有可能性，如下代码就是错的： fn plus_one(x: Option<i32>) -> Option<i32> { match x { Some(i) => Some(i + 1), // 没讨论是None的情况 } }if let:这个操作符能简化Match的写法，比如如下代码：let config_max = Some(3u8); match config_max { Some(max) => println!("The maximum is configured to be {}", max), _ => (),能简写成：let config_max = Some(3u8); if let Some(max) = config_max { println!("The maximum is configured to be {}", max); }看到这里可能有人会问为啥不直接if Some(max) == config_max，这里千万要注意Some(max)并不是一个变量，而是解包操作！结语相信大家看到这里已经对Rust有了一个初步的理解。然而除了这些内容咱还有很多知识点没能探讨到，比如：泛型，多线程，智能指针，错误处理等等...这些内容我会放在未来的“Rust后日谈”文章探讨，敬请期待！
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 CPUs exist when in fact there is only one physical CPU (or a few). This basic technique, known as time sharing of the CPU, allows users to run as many concurrent processes as they would like.mechanisms: are low-level methods or protocols that implement a needed piece of functionality. Int he CPU virtualizing aspect, the mechanisms involved are:context switchtime-sharingscheduling policy...machine state: what a program can read or update when it is running.memory, or more specifically: the address spaceprogram counter (PC), also called as instruction pointer or IPstack pointer and frame pointer, use to manage the stack fro function parameters, local variables and return addressAPICreate: method to create new processDestroy: come with createWait: Sometimes it is useful to wait for a process to stop running; thus some kind of waiting interface is often providedMiscellaneous control: method to suspend a process (stop it from running for a while) and then resume it (continueit running).Status: information about a process, how long it has run for, or what state it is inProcess CreationThe first thing that the OS must do to run a program is to load its code and any static data (e.g., initialized variables) into memory, into the address space of the process.Once the code and static data are loaded into memory, there are a few other things the OS needs to do before running the process. Some memory must be allocated for the program’s run-time stack (or just stack). The OS may also create some initial memory for the program’s heap.The OS will also do some other initialization tasks, particularly related to input/output. For example, in UNIX systems, each process by default has three open file descriptors: input, output and errorProcess StatesIn a simplified view, a process can be in one of three states:Running: the processor is executing instructionReady: the process is ready but for some reason the OS has chosen not to run itBlocked: process has performed some kind of operation that makes it not ready to run until some other event takes place.Process: states transitionsData structureTo track the state of each process, for example, the OS likely will keep some kind of processlist for all processes that are ready, as well as some additional information to track which process is currently running. The OS must also track, in some way, blocked processes; when an I/O event completes, the OS should make sure to wake the correct process and ready it to run again.// the registers xv6 will save and restore // to stop and subsequently restart a process struct context { int eip; int esp; int ebx; int ecx; int edx; int esi; int edi; int ebp; }; // the different states a process can be in enum proc_state { UNUSED, EMBRYO, SLEEPING, RUNNABLE, RUNNING, ZOMBIE }; // the information xv6 tracks about each process // including its register context and state struct proc { char *mem; // Start of process memory uint sz; // Size of process memory char *kstack; // Bottom of kernel stack // for this process enum proc_state state; // Process state int pid; // Process ID struct proc *parent; // Parent process void *chan; // If non-zero, sleeping on chan int killed; // If non-zero, have been killed struct file *ofile[NOFILE]; // Open files struct inode *cwd; // Current directory struct context context; // Switch here to run process struct trapframe *tf; // Trap frame for the // current interrupt };Interlude: fork()when a process execute fork(), the process that is created is an (almost) exact copy of the calling process, and run two processes on OS. Because of that, the process is not deterministic because of the scheduler (you don't know which process runs first).Mechanism: Limited Direct ExecutionIntroduce how CPU share physical CPU among many jobs running seemingly at the same time.Questions need to figure out: Performance: implement virtualization without adding excessive overhead to the system. Control: how can we run processes efficiently while retaining control over the CPU. The basic technique to solve this to solve the questions is Limited Direct Execution. The “direct execution” part of the idea is simple: just run the program directly on the CPU. Thus, when the OS wishes to start a program running, it creates a process entry for it in a process list, allocates some memory pages for it, loads the program code into memory, disk), locates its entry point (i.e., the main() routine or something similar), jumps to it, and starts running the user’s code.Problemssome problems introduced by the limited direct execution mechanismRestricted Operationshow to prevent the UserApp running some restricted operations?We can solve it by introducing a new processor mode: user mode; code that runs in user mode is restricted in what it can do. For example, when running in user mode, a process can’t issue I/O requests; doing so would result in the processor raising an exception; the OS would then likely kill the process.In contrast to user mode is kernel mode, which the operating system (or kernel) runs in. In this mode, code that runs can do what it likes, including privileged operations such as issuing I/O requests and executing all types of restricted instructions.For UserApp to access privileged operation, they can perform the system call, which allow the kernel to carefully expose certain key pieces of functionality to user programs, such as accessing the file system, creating and destroying processes, communicating with other processes, and allocating more memory.To execute a system call, a program must execute a special trap instruction. When finished, the OS calls a special return-from-trap instruction, which, as you might expect, returns into the calling user program while simultaneously reducing the privilege level back to user mode.Switching between processesHow can the operating system regain control of the CPU so that it can switch between processes?Approach 1: Cooperative, wait for system calls: the OS trusts the processes of the system to behave reasonably. Processes that run for too long are assumed to periodically give up the CPU so that the OS can decide to run some other task. Applications also transfer control to the OS when they do something illegal. For example, if an application divides by zero, or tries to access memory that it shouldn’t be able to access, it will generate a trap to the OS.Approach 2: Non-Cooperative: we can use the timer interrupt and set it to every processes, timer device can be programmed to raise an interrupt every so many milliseconds; when the interrupt is raised, the currently running process is halted, and a pre-configured interrupt handler in the OS runs. At this point, the OS has regained control of the CPU, and thus can do what it pleases: stop the current process, and start a different one.scheduler: decide whether to continue running the currently-running process, or switching to a different one.context switch: if the system make the decision to switch processes, the OS will execute a lower level piece of code which refer to a context switch, all the OS has to do is save a few register values for the currently-executing process (onto its kernel stack, for example) and restore a few for the soon-to-be executing process (from its kernel stack).
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; }
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 with parameters p and q. Write:$$ x=\frac{h-Np}{\sqrt{Npq}} $$The, for large N, the probability distribution $P(x)$ can be approximated by the probability density function:$$ P(\{x\in [a,b]\})\approx \int^b_a(\frac{1}{\sqrt{2\pi}})\text{exp}(\frac{-x^2}{2}) $$Experimentpopulation and sample: if we could have seen everything, is the population. I will write populations like random variables with capital letters to emphasize we don’t actually know the whole population. The data we actually have is the sample.sample mean: the mean from sample, usually notated as: $X^{(N)}$: sample mean when sample size is $N$it is a random variable$\mathbb{E}[X^{(N)}]=\text{popmean(\{X\})}$$var[X^{(N)}]=\frac{\text{popsd(\{X\})}^2}{N}$$std[X^{(N)}]=\frac{\text{popsd(\{X\})}}{\sqrt{N}}$confident interval:confidence interval for a population mean: Choose some fraction f, An f confidence interval fora population mean is an interval constructed using the sample mean. It has the property that for that fraction f of all samples, the population mean will lie inside the interval constructed from each sample’s mean.centered confidence interval for a population mean: Choose some$0<\alpha<0.5$. A $1-2\alpha$ centered confidence interval for a population mean is an interval $[a,b]$; b constructed using the sample mean.unbiased standard deviation: use to estimate the population standard deviation$$ \text{stdunbiased(\{x\})}=\sqrt{\frac{\sum_i(x_i-\text{mean}(\{x\})^2)}{N-1}} $$standard error: The standard deviation of the estimate of the mean$$ \text{stderr}(\{x\})=\frac{\text{stdunbiased(\{x\})}}{\sqrt{N}} $$Random variable distributionwe learn two distribution for random variable for far: the t-distribution and normal distribution, depended on the sample size, if $n<30$, we use t-distribution, otherwise use normal distributiont-distribution:$$ T=\frac{\text{mean}(\{x\})-\text{popmean(\{X\})}}{\text{stderr(\{x\})}} $$degree of freedom: $N-1$normal distribution:$$ Z=\frac{\text{mean}(\{x\})-\text{popmean(\{X\})}}{\text{stderr(\{x\})}} $$degree of freedom: $N$Practice Question附件附件名称：cs361 mid2 achieve.zip文件大小：348.5 KB下载次数: 516最后修改: 2023-04-04 16:01点击下载
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 amount of dataprocess:scan DB, find single item frequent patternsort frequent item in frequent descendingscan DB again, find the ordered frequent itemlist for each transactionFP growth treeFP-growth is faster than Apriori for most of situationsboth FP and Apriori are mining from horizontal data format (TID: data)Pattern Evaluatelift: Measure of dependent/correlated events$$ lift=\frac{s(B\cup C)}{s(B)\times s(C)} $$$lift(B, C) = 1$: B and C are independent$> 1$: positively correlated$< 1$: negatively correlated$\chi^2$: another way to measure test correlated events$$ \chi^2 =\sum\frac{(Observed -Expected)^2}{Expected} $$sample datachi square calculationfor both $\chi ^ 2$ and lift measure, they might be influenced by null transactionsNull invariance: The number of null transactions does not matter, does not change the measure value.correlation formulasImbalance Ratio (IR)measure the imbalance of two itemsets A and B in rule implications$$ IR(A,B)=\frac{|s(A)-s(B)|}{s(A)+s(B)-s(A\cup B)} $$if $IR=0$, means two events are balancedLift and χ2 are good measures if null transactions are not predominantOtherwise, Kulczynski + Imbalance Ratio should be used to judge the interestingness of a patternMining Multilevel Patternsmin-support: there are two min-support thresholdsuniform: same min-support across multiple levelslevel-reduced: min-support reduced as level become lowerredundancy filtering: redundant due to “ancestor” relationshipsA rule is redundant if its support is close to the “expected” value, according to its “ancestor” rule, and it has a similar confidence as its “ancestor”milk $\rightarrow$ wheat bread [support = 8%, confidence = 70%] (1)2% milk $\rightarrow$ wheat bread [support = 2%, confidence = 72%] (2)Suppose the 2% milk sold is about ¼ of milk sold in gallons, then, the data above is redundantcustomized min-supports: to analyze the item with less frequency (low support), we can use group-based min-support{diamond, watch}: 0.05%; {bread, milk}: 5%quantitative associations:methods used when mining associations with numerical attributesStatic discretization: age: {0-10, 10-20, ..., 90-100} → {young, mid-aged, old}Dynamic discretization based on data distributionClustering: Distance-based associationDeviation analysis: Gender = female $\rightarrow$ Wage: mean=$7/hrmining extraordinary phenomena:check if LHS (a subset of the population) behave extraordinarily compared to RHS (an extraordinary behavior of this subset)The rule is accepted only if a statistical test (e.g., Z-test) confirms the inference with high confidencenegative pattern: Unlikely to happen togetherIf itemsets A and B are both frequent but rarely occur together, then:$$ s(A\cup B) << s(A)\times s(B) $$the equation above will be influenced by the null transaction, we can use Kulczynski-measure:If itemsets A and B are frequent but: ($є$: negative pattern threshold)$$ (\frac{s(A \cup B)}{s(A)} + \frac{s(A \cup B)}{s(B)})\cdot \frac{1}{2} < є $$then A and B are negatively correlated.Constraint-Based MiningMine together with user-provided constraintstype of constrains:Knowledge type constraint—Specifying what kinds of knowledge to mineData constraint—using SQL-like queriesDimension/level constraint—similar to projection in relational databaseInterestingness constraint—various kinds of thresholdsRule (or pattern) constraintcharacteristic of constrain:Anti-Monotonicity: set violated, then its superset must violate as well e.g. $support(S) \rightarrow \sigma$Monotone: if set satisfied, then its superset must satisfied as well. e.g. $sum(S.Price) \rightarrow v$Convertible: Convert tough constraints into (anti-)monotone by proper ordering of items in transactions. e.g. $avg(S.profit)>20$Data anti-monotone: In the mining process, if a data entry t cannot contribute to a pattern p satisfying c, t cannot contribute to p’s supersetSuccinctness: If the constraint c can be enforced by directly manipulating the dataData succinct: Data space can be pruned at the initial pattern mining processpruningconstrain type p1constrain type p2Download Note附件附件名称：midterm2 note.zip文件大小：754.1 KB下载次数: 605最后修改: 2023-03-29 22:41点击下载