## Records for 4-5 and 4-6

Dancing disco at the cementry.

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: ## 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$ $\Delta X_0 = \left(\left.\frac{\partial F}{\partial X}\right|_{X=X_0}\right)^{'}F(X_0)$ $X_1=X_0+\Delta X_0$ Likewise, $X_2=X_1+\Delta X_1$ 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.

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:

And an implementation of it:

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

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

And an implementation by list here:

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.

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:

$*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:

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