Implicits resolution rules and examples

http://eed3si9n.com/revisiting-implicits-without-import-tax

Some video links

Verification of Computer Systems with Model Checking
by Ed. M. Clark, at FloC 2014 keynotes

Transducers by Rich Hickey

JavaScript tricks

Duck typing

You can invoke an object's method on another object, as long as the latter has everything the method needs to operate properly. Example:

function foo() {
  // the last element of arguments is popped
  Array.prototype.forEach.pop.bind(arguments)();
  // this works as if arguments had a "forEach" method
  Array.prototype.forEach.bind(arguments)(function(a){ console.log(a) }); 
}

Dynamic scoping

The easiest way to archive dynamic scoping in JavaScript is to use eval:

var x = 1;
function g() {
  console.log(x);
  x = 2;
}
function f() {
  // create a new local copy of `g` bound to the current scope
  var x = 3;
  eval(String(g));
  g();
}
f();             // prints 3
console.log(x);  // prints 1

Perhaps this is one of the few valid reasons to use eval in JavaScript.

Loose augmentation

Suppose that you have several module files that share a MODULE variable. Then it is preferable to let organize each module file like

var MODULE = MODULE || {}; // MODULE is always declared due to hoisting
(function() { 
  var private_var;         // only accessible to myFunction
  MODULE.myFunction = ...  // augment the module with a new function 
})();

In this way, you can load all of your module files asynchronously without the need to block, given that the functions defined in the module don't depend on each other.

Call-site memorization

The word memoization refers to function-level caching for repeating values. Suppose we have a function G such that G(f) will compute an expensive function f many times. If f is pure, then we can cache the results of f without modifying G or introducing global variables. Instead of calling G(f) directly, we pass to G a closure of f as follows:

var memorize = function(f) {
  var cache = {};
  return function(x) {
    if(!cache.hasOwnProperty(x))
      cache[x] = f(x);
    return cache[x];
  };
};
G(memorize(f));

The use of cache here is totally transparent from the view of G. Note: You may want to use an LRU/LFU cache to avoid running out of memory.

Gorogoa

Blog of the designer

Three years passed... when will this game be released?

Tricks in solving common programming problems

O(1)-space collision detection

At times, you need to detect for once whether a collision occurs. For example, you may need to enumerate a sequence$$ x_0,\ x_1=f(x_0),\ x_2=f(x_1),\ \dots,\ x_i=f(x_{i-1}),\ \dots $$until either a desired element is found or a cycle is detected. A naive method to detect a cycle requires storing all elements ever enumerated in a hash table. This method however would need to store the entire sequence in the worst case. Instead, you can utilize one of the cycle detection techniques to reduce the space to O(1) at the cost of possibly longer search time.

(more to come...)

Quantifier elimination

A theory has quantifier elimination if for every formula f of the theory, there exists another formula f' without quantifiers that is equivalent to it (modulo the theory).

A common technique to show that the validity of a theory is decidable is to show that the theory admits decidable quantifier elimination and then prove the decidability of quantifier-free sentences. This technique is used to show that Presburger arithmetic, i.e. the theory of the additive natural numbers, is decidable.

Note that theories could be decidable yet not admit quantifier elimination. For example, Example: Nullstellensatz in ACF and DCF. On the other hand, whenever a theory in a countable language is decidable, it is possible to extend its language with countably many relations to ensure that it admits quantifier elimination.

Compiling Z3py on Windows

1. git clone Z3.

2. Install Python. (Either 2.x or 3.x is fine.)

• Note that you have to install 64bit/32bit Python runtime on a 64bit/32bit machine; for otherwise the Z3py library would not initialize (would show a "dll not found" message).

3. Install Visual Studio Community if you don't have Vitual Studio installed. Add the command-line tools of VS to your PATH environment variables.

4. Install Windows SDKs for libraries.

5. Setup environment variables in Cygwin for nmake.

• On my computer, I set these two:

  LIBPATH="C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\lib"
  INCLUDE="C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\include;C:\Program Files (x86)\Microsoft SDKs\Windows\v7.1A\Include"
  

6. Configure and nmake Z3

• I have to remove BOM in file z3\src\api\dotnet\Properties\AssemblyInfo to resolve a decoding problem.

7. Done.