Artificial Intelligence

Resolution

If $l_i \Leftrightarrow \neg m_j$, then:

If there is a empty clause after a resolution, it means there are conflicts.

Resolution algorithm to prove $\alpha$ within KB:

1. Generate CNF of the knowledge base $KB\wedge\neg\alpha$
   • CNF: $(l_{1,1}\vee l_{1,2} \vee \cdots \vee l_{1,n_1}) \wedge (l_{2,1}\vee \cdots \vee l_{2,n_2})\vee\cdots \vee (l_{m,1}\vee\cdots\vee l_{m,n_m})$
   • Also called k-CNF if $n_1 = n_2 = \cdots = n_m = k$
2. Repeat resolution process for every new rule
   1. If there is no new rule, $\alpha$ cannot be proved.
   2. If there is an empty literal, then stop and $\alpha$ is proved

Complexity: exponential

Expressiveness: better (not restricted to Horn clauses)

Propositional logic

Jargons

Use functions, predicates to represent relationships:

• A is a person -> $Person(A)$, Person: predicate
• Person a has a crippled left leg -> $Crippled(LeftLegOf(a))$, LeftLegOf: function (it’s OK since a human has only one left leg) Formally,

Term ::= Function ( Term {, Term}* ) AtomicSentence ::= predicate ( Term {, Term}* ) …

Model

Forgot that.

Networking

Cisco’s proprietary software, packettracer, couldn’t be downloaded without enrolling in its network course.

IOS

• use enable to enable the thing
• show interfaces to have a look at all interfaces, show interface [interface].
• show vlan to show vlan
• configure terminal to open the configuration in terminal
• (config) interface [interface] to select an interface

Dynamic Trunking Protocol

A proprietary protocol invented by Cisco to negotiate trunking on a link between two VLAN-aware switches.

There is several modes for it:

• access: puts the ethernet port into non-trunking mode and negotiates to convert the link to a nontrunk one, disregarding the neigboring port
• trunk: puts the ethernet port into trunking mode and negotiates to convert the link to a trunk one, disregarding the neigboring port
• dynamic auto: willing to trunk, will be trunk if the neighboring port is dynamic desirable or trunk
• dynamic desirable: actively willing to trunk
• nonegotiate: disable DTP. No wonder, it is not compatible with dynamic modes.

Except nonegotiate, all modes are triggered by (config-if) switchport mode [mode]. Switch to no-negotiate mode using (config-if) switchport nonegotiate.

Use a no before the statement to do the opposite thing, like:

(config-if) no shutdown: set up the link (config-if) no switchport nonegotiate: turn on DTP

Computer Graphics

Blurring is often used in computer graphics, like, to create HDR(high dynamic range) bloom, depth of field or other post process effects.

HDR bloom: since the real-world camera cannot focus perfectly, so it will convolve the incoming image with an Airy disk. What about the Airy disk? Know what a spot of light looks like in our eyes? That would be one. A perfect lens with a circular aperture would make it because the diffraction of light.

This effect is not noticeable when it is not so bright. However, with more light we can see the blurred edge of the bright part of the image, taken by a camera. And computer graphics tries to reproduce the same effect by blurring.

You can think up an approach instantly: take the average of neighboring blocks, like below:

By all means this is bad. It will seem block-ish.

A better one is Gaussian blur. It uses the Gaussian distribution as the weight of neighboring pixels to calculate the average, or more accurately, do the convolution. The weight matrix, like the one above, is called kernel.

A 3x3 Gaussian kernel is like:

Some other kernels are here.

It also can be used before downsampling: Gaussian blur gets rid of the sharp edges in the image, thus after downsampling, it will free the image from aliasing like moire patterns. Aliasing happens because of the poor sampling makes different signals indistinguishable, and some high frequency signals might get in the way after sampling. So a low pass filter need to be applied before sampling.

Task: sample => downscale image Reason of problem: high freq. signal => ? Problem: aliasing => moire pattern Solution: low pass filter => blurring

And yes, Gaussian blur is also a low pass filter, with a Bode plot like a parabola. Possibly it seems obvious at first sight: Gaussian distribution has a factor $e^{-\frac{x^2+y^2}{2\sigma^2}}$, which is stable through Fourier transforms.

We can calculate it out. Let’s put the basic calculus into practice.

So the amplification is:

Perfect! It is a parabola after all.

Leave Kawase to the next day.

Misc

マシンガンでも壊せなくて キャタピラーでも潰せなくて

Comment and share

Database

PL/SQL

Anonymous and named PL/SQL block

• Anonymous PL/SQL block
  • Need to compile every time
  • Not stored
• Named PL/SQL block
  • Can be stored in DB

Stored Procedure

Grammar:

Procedure ::= CREATE [OR REPLACE] PROCEDURE ProcedureName '(' Parameters ')' (AS|IS) RETURN ReturnType DECLARE Declaration BEGIN Body END ';'
Parameters ::= Nothing | Parameter {, Parameter}
Parameter ::= ParameterName (IN|OUT|IN OUT) Type ':=' DefaultValue

• Note:
  • In the parameter list, varchar cannot be specified with a length.
  • MySQL has no AS|IS in the procedure, and IN/OUT is put before the parameter name.
  • In MySQL ,one has to change the delimiter before defining a procedure or function.

Loop statement

• for x in [Reverse] 1…20 loop … end loop;
• while … loop … end loop; To escape from a loop:
• exit when …;

Conditional statement

• if … then … elseif … end if;

Cursor

• Used to process a set of records. PL/SQL record variable can only store one record at a time.
• Technically, it acts like an iterator, which means one cannot process multiple records at the same time(though we can store them as a whole).
• In declaration, a cursor is declared with a SELECT statement, and we can use this cursor to access the data returned by that SELECT statement
• A cursor is bind to one specific SELECT clause, that is, one cannot bind it to another SELECT statement
• The SELECT statement is and only is executed when the cursor is OPENed(see below).
• CLOSE the cursor to free the memory space. Synopsis:

1. Declaration

cursor cursor_name is select statement;

2. Open cursor

OPEN cursor_name;

3. Get the data

FETCH cursor_name into variable;

• The cursor will move forward, just like python’s next function do.

4. Check if there is no more entry

IF NOT cursor_name%FOUND THEN …;

5. Close the cursor

CLOSE cursor_name;

6. For loop Unique to Oracle. No need to open, close, or fetch from a cursor.

FOR variable in cursor_name LOOP – do something to the variable END LOOP;

Artificial Intelligence

Knowledge base && Inferrence

* Truth table

* Brute force search

* Forward chaining
    * reliable
    * completeness
        * -> only have these two properties for the knowledge bases able to be expressed with Horn clauses
        * Horn clause: a disjunction of literals with at most one unnegated literal
            * E.g. {% katex %}
\neg x_1 \vee \neg x_2 \vee \cdots \vee x_n \vee u
{% endkatex %}

* Backward chaining
    * To prove q, with p->q now prove p
    * Avoid repeating by check if a clause is already proved or disproved

Misc

Panning derives from panorama.

4/11 Record

Programming Languages

Polymorphic Functions

• Static: cost grows exponentially with parameters
• Dynamic:
  • supply a tag when calling the function

Example: Overloading Equality

1. Equality was overloaded as an operator
2. Make type of equality fully polymorphic
3. Make equality polymorphic in a limited way
   • (==) :: ''t -> ''t -> Bool, ''t is a type t with equality
   • will be a static error if t is not Eq type

Type Classes

1. Merchanism in Haskell
2. Dictionary-passing style implementation [ESOP1988]
   • Type class declaration – dictionary
   • Name of a type class method – label in the dictionary
   • Parametric overloading – passing the dictionary to the function

class Show a where
    show :: a -> String

instance Show Bool where
    show True = "True"
    show False = "False"

print :: Show a => a -> IO ()
print x = putStrLn $ show x

type 'a show = {show: 'a -> string}
let show_bool : bool show = 
{
    show = function
        | true -> "True"
        | false -> "False"
}

let print : 'a show -> 'a -> unit =
    fun {show=show} x -> print_endline (show x)

Smalltalk: subtyping

• Object -> super class -> method table

• If interface A contains all of interface B, then A objects can also be used as B objects

  • need to look up all instances(members) at runtime

Javascript has the same problem

• v8 engine: hidden class

function Person(first_name, last_name) {
    this.first_name = first_name;
    this.last_name = last_name;
}

var potus = new Person('D.', 'Trump');
var potrf = new Person('V.', 'Putin');

Computer Architecture

Optimizing cache

Merging write cache

DRAM and SRAM

Misc

最低だ　最低だ　最低だ

Comment and share

Records for 4-5 and 4-6

Dancing disco at the cementry.

About Mathematica

Mathematica 11 could not be started after a freetype upgrade.

When run in command line, it emits an error like this.

According to the gentoo forum site. Mathematica has its own libraries, and it calls the system library of freetype.

Forcing Mathematica to use the system library by removing libfreetype.so.6 and libz.so.1 in ${TopDirectory}/SystemFiles/Libraries/Linux-x86-64 could solve the problem.

About R

To do a linear fit by this:

x <- c(...)
y <- c(...)
fit <- lm(y ~ x)

The one who wrote this article fell asleep halfway…

Rec 4.8

Computing Method

If f(x) satisfies:

1. $f(x) \in [a, b], x \in [a, b]$
2. $f'$ is Lipschitz continuous with some $K < 1$.

Then there exists a unique fixed point of f in $[a, b]$.

Existence: intermediate value theorem.

Uniqueness: reductio ad absurdum.

Newton’s method:

To find $X$ s.t. $F(X) = 0$.

First $X=X_0$

Likewise,

…

Where $\frac{\partial F}{\partial X}$ is the Jacobian matrix of $F$.

Facts about Mozilla

• It developed Thunderbird, a program for emails, feeds, and IM and so on. And now Thunderbird is abandoned.

Firefox

It is said starting firefox with env MOZ_USE_XINPUT2=1 firefox enables scrolling with a finger. Not working now.

The bugzilla page suggests there should be a --enable-default-toolkit=cairo-gtk3 in the configure options shown in about:buildconfig.

Works now after upgrading GTK. Why.

Firefox OS

Another abandoned project is Firefox OS. Refer to this post.

• Starting point: Boot to Gecko(B2G), push the envelop of the web

  • Architecture:
    • Gonk: Open Linux kernel and drivers
    • Gecko: Web runtime with open Web APIs
    • Gaia: User interface with HTML5-based Web content

• Firefox OS 1.0

  • Imitate what already existed
  • Invented a lot of APIs to talk to hardware of a smartphone from Javascript(that wouldn’t come into standards)
  • Introduced packaged apps to Gecko to achieve both the offline(run apps without Internet connection) and security requirements(to secure privileged functions like calling and texting messages).
    • Packaged apps got no URLs and have to be signed by a central authority to say they are safe. -> Against the web.

• Firefox OS 1.x

  • Just chasing the coat tails of Android

• Differentiation

  • Affordable phones -> 1.3t
    • $25 smartphone: mostly done by Taipei office
  • Web -> 2.0
    • Haida: blur the line between apps and websites
    • Overshadowed by feature requests from venders

• 3.0 -> 2.5 Come to stall and dead in the end.

Rec 4.9

Computer Architecture

Refer to Computer Architecture: A Quantitative Approach

Optimization of Cache Performance

1. Nonblocking Caches to Increase Cache Bandwidth

Pipelined computers that allow out-of-order execution will benefit from this kind of cache which can supply cache hits even during a miss.

2. Multibanked Cache

Increase bandwidth.

3. Compiler

4. Prefetching

Programming Languages

Still, refer to Standford’s cs242.

Existential types

Interface: specify what a type should be able to do, regardless of the implementation

Implementation: concretize the interface by showing how a type can implement the interface

It has two kinds of operations: pack and unpack.

Packing is the introduction of an implementation(see More monads in OCaml).

For example, this is an example of a monad interface:

module type M = sig
    type _ t
    val pure : 'a -> 'a t
    val bind : ('a -> 'b t) -> 'a t -> 'b t
end;;

And an implementation of it:

module Option:M = struct
type 'a t = Nothing | Just of 'a
let pure x = Just x
let bind f x = match x with
| Just y -> f y
| Nothing -> Nothing
end;;

It’s an ugly example, but the point is, the detail about Option.t is erased, with only the interface(pure, bind) left.

utop # Option.pure 3;;
- : int Option.t = <abstr>

The implementation, Just 3 is not available here, and we cannot use Just to create a Option.t as well. Wait … shit.

Forget about monads, let’s go with another example:

module type Stack = sig
    type _ t
    val create : unit -> 'a t
    val push : 'a t -> 'a -> 'a t
    val pop : 'a t -> 'a t * 'a option
    val empty : 'a t -> bool
end;;

And an implementation by list here:

module LStack : Stack = struct
    type 'a t = 'a list
    let create = fun () -> []
    let push s x = x::s
    let pop x = match x with
        |x::xs -> xs, Some x
        |[] -> [], None
    let empty x = match x with
        |x::xs -> false
        |[] -> true
end;;

Everything works fine without the knowledge that LStack uses list for the stack. Say you create a new stack using LStack.create, there is no way for you to use it as a list, though it is one.

utop # let mystack = LStack.create ();;
val mystack : '_a LStack.t = <abstr>
utop # assert(mystack=[]);;
Error: This expression has type 'a list but an expression was expected of type
         'b LStack.t

That’s abstraction in a nutshell.

The existential type is like this: ${*S, t} : {\exists X, T}$ means that type t, coupled with implementation S, makes a package that have an abstract type X with signature T. For the LStack, the analogy would be:

And there is the pack operation, which erases one or more types and introduces an implementation:

Misc

愛されたくて偽って　もっともっと自然に笑えばいいかな

Comment and share

Computer Architecture

• Cache Optimization
  • Lower 3C:
    • +cache block size -> -compulsory -> +conflict
    • +cache capacity -> -capacity caused misses -> hit time
    • +associativity -> +parallel comparison
  • Lower cost of cache miss:
    • multi-layer cache(victim cache)
      • global miss rate vs. local miss rate, AMAT
      • If L2 cache is much larger than L1, the global miss rate is close to that with a single level cache of L2’s size
      • placeholder
  • placeholder
    • Small and simple first level caches
    • Critical timing path:
    • Direct-mapped caches can overlap tag compare and transmission
    • placeholder

Programming Languages

Refer to this page.

Since in OCaml the content of a function is not evaluated in its definition, the approach could be used to create lists with infinite length.

type 'a list = Nil | Cons of 'a * (unit -> 'a list);;

The good thing about it is that the function is not evaluated at once, so the infinite recursion is avoided.

And there is some other utilities:

let head x = let Cons(a, _) = x in a;;

let tail x = let Cons(_, b) = x in b ();;

let rec take n x = match n, x with
| _, Nil -> []
| 0, _ -> []
| n, Cons(h, tf) -> h :: take (n-1) (tf ());;

let rec drop n x = match n, x with
| _, [] -> []
| 0, x -> x
| n, Cons(h, tf) -> drop (n - 1) (tf ());;

let rec fmap f x = match x with
| Nil -> Nil
| Cons(h, tf) -> Cons(f h, fun () -> fmap f (tf ()));;

Note that () is of type unit in OCaml, not () in Haskell.

And we can have something like 1... now in OCaml:

let rec toinf = fun x -> Cons(x, fun () -> toinf (x + 1));;

Or better, some Fibonacci series:

let rec fib = fun x y -> Cons(x, fun () -> fib y (x + y));;

Argh.

This one, though it looks elegant, would run slow.

let rec toinfslow x = Cons(x, fun () -> fmap ((+) 1) (toinf x));;

Imagine: you get 20 in toinfslow 10 by adding to it 1 ten times.

And a even slower Fibonacci series:

let rec fibslow x y = Cons(x, fun () -> Cons(y, fun () -> sum (fibslow x y) (tail (fibslow x y))));;

Go with take 40 (fibslow 1 1) and you would not get the result as fast as the first one.

OCaml has a lazy module that would delay the evaluation of the expression, and also cache the result. So a lazy list would be faster after calculating once.

About Hacking Conferences

Chinese government has banned its security researchers from participating foreign security conferences this year, and Pwn2Own on Mar. 12-14, which Chinese dominated for years, was impacted by this new policy. And Zhou Hongyi, chief executor of 360, has previously stated that these loopholes ‘should remain in China’.

Learning Kana Input…

ろぬふあう　えおやゆよ　わほへ ` 1 2 3 4 5 6 7 8 9 0 - =

たていすか　んなにらせ　゛゜む q w e r t y u i o p [ ] \

ちとしはき　くまのりれ　け a s d f g h j k l ; ’

つさそひこ　みもねるめ z x c v b n m , . /

Use shift key for smaller kana. E.g. ゃ is entered with Shift + 7.

Misc

Was yea erra hymme sarla yorr.

About Vocaloid

• Kemu was probably once troubled by Suzumu, a member of Kemu VOXX, and who had a similar style. Kemu came back with Haikei Doppelganger in 2017, which possibly refers to Suzumu.

• After the admitting the ghostwriting of some of his songs, Suzumu announced that he would retire from making vocaloid songs in 2017. Which means the Bookmark of Demise Project stopped without ending.

• Mafumafu is said to had bad terms with Suzumu, which brought a lot damage to him.

• Powapowa-P, a.k.a. Shiina Mota, deceased at 20, with a red pen. The cause of his death was not revealed.

• Samfree died at 31 from illness. Recommend his Promise, although a lot may have already known it from Project Diva.

Comment and share

Records from 3/29 to 4/2

To be filled…

Facts about SQL

• MySQL does not support data integrity check(that is, it parses but ignores CHECK constraint).
• MariaDB was the same but started implementing it since 10.2.
• PostgreSQL is likely to support this feature.

Facts about Arch Linux

• Arch Linux has only in its official repo MariaDB 10.1 because of this.
• updpkgsums is a command line tool to update the checksums in the PKGBUILD file.
• Running makepkg with -s would install the dependencies for it, and -i would install the package built.
• trizen, aurman are also AUR helpers, the same as yaourt, pacaur.

Facts about CentOS 7

• It uses Linux 3.10.
• The packages in EPEL can be very old as well.
• The lttng package in EPEL is ver 2.4.

Fact about Oracle

It sucks.

Facts about Input Methods

• The author of Flypy(http://www.flypy.com) is stingy about the double pinyin scheme they created – they haunt every developer of an input method which make Flypy available – either as preset or configurable afterwards – without their authorization.

• Rime, GBoard, and MS IME seem not (yet) in trouble.

• The author of Flypy criticized others’ approach to tackle zero-consonant characters(‘a’, ‘er’, ‘ou’, etc.) from their perspective. Flypy uses the first and the last letter of the syllable(‘ee’ for ‘e’, ‘ag’ for ‘ang’, etc.), while some others allocate a specific letter, say, ‘o’, for it.(That is, ‘oa’ for ‘a’, ‘ol’ for ‘ai’ for MS).

• A family of double pinyin derives from Ziranma, with minor differences. MS and Sogou are among them.

• Mozc could be configured using /usr/lib/mozc/mozc_tool --mode=config_dialog, where the input mode could be switched between Romaji and Kana.

Misc

空はきれいなのに

Comment and share