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 and 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)[a,b],x[a,b]f(x) \in [a, b], x \in [a, b]
  2. ff' is Lipschitz continuous with some K<1K < 1.

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

Existence: intermediate value theorem.

Uniqueness: reductio ad absurdum.

Newton’s method:

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

First X=X0X=X_0

ΔX0=(FXX=X0)F(X0)\Delta X_0 = \left(\left.\frac{\partial F}{\partial X}\right|_{X=X_0}\right)^{'}F(X_0) X1=X0+ΔX0X_1=X_0+\Delta X_0


X2=X1+ΔX1X_2=X_1+\Delta X_1

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

Facts about Mozilla

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


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.

  1. Multibanked Cache
Bank 1 Bank 2 Bank 3 Bank 4
0 1 2 3
4 5 6 7
8 9 10 11
12 13 14 15

Increase bandwidth.

  1. Compiler

  2. 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

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

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

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

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:X,T{*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:

listS{create=,push=,pop=}t{create:a.unitX[a], push:a.X[a]aX[a], pop:a.X[a]X[a]option[a]}T *list \sim *S\\ \{create = \cdots, push = \cdots, pop = \cdots\} \sim t\\ \{create : \forall a.unit \rightarrow X[a],\ push : \forall a.X[a] \rightarrow a \rightarrow X[a],\ pop : \forall a.X[a] \rightarrow X[a] * option[a]\}\sim T

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

Γt:[XU]TΓ{U,t} as {X,T}:{X,T}\frac{\Gamma \vdash t : [X\rightarrow U]T}{\Gamma \vdash \{*U, t\}\ as\ \{\exists X, T\} : \{\exists X, T\}}


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