banacorn

• Steuerausländer 國外納稅人？：

  我在此確認，我在德國境內沒有住處（Wohnsitz）而且也沒有經常居住事實（gewönlichen Aufenthalt），因此不須盡繳納所得稅之義務（einkommensteuerpflichtig）

  • 在此附上從德國政府登記單位？（deutschen Meldebehörder）的註銷授權（Abmeldebescheinigung）（否則可能會不被當作 Steuerausländer。）
  • 我持有其他歐盟國家（非德國）的身分證明（Ausweis），並且在歐盟以外有住處。在此附上那住處（由那地方具證明能力的政府單位所發出）的證明（否則要接受 EU-ZIV （Zins 利息？Infomation 資訊？EU Verorden 歐盟規章）的強制登記（Meldepflicht）。）
  • 儘管我在國內有住址，但因為一些特殊的緣故，把我當作國外納稅人 @@

• Steuerinländer 國內納稅人：

我在德國境內有住處或經常居住事實因此須盡德國繳稅義務，或因為其他原因須盡德國繳稅義務

banacorn

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, GADTs
           , OverlappingInstances, FlexibleInstances, UndecidableInstances
           , MultiParamTypeClasses
           #-}

import GHC.TypeLits
import Data.Type.Equality
import Data.Proxy

--------------------------------------------------------------------------------

banacorn

# courtesy of @jccguimaraes, https://gist.github.com/jccguimaraes/2e08be6f549448d9361c
path    = require 'path'
Mocha   = require 'mocha'

module.exports = (args) ->
    promise = new Promise (resolve, reject) ->

        # build a headless Atom
        window.atom = args.buildAtomEnvironment
            applicationDelegate: args.buildDefaultApplicationDelegate()

banacorn

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

-- definition of List
data List (A : Set) : Set where
    []  : List A
    _∷_ : A → List A → List A

-- "fold", or "reduce" in python

banacorn

{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, PolyKinds, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, OverlappingInstances #-}

module Sandbox2 where

import GHC.TypeLits
import Data.Proxy

--------------------------------------------------------------------------------
--  Heterogeneous list
--------------------------------------------------------------------------------

banacorn

open import Data.Char
open import Data.List
open import Function using (flip; _$_)
open import Relation.Nullary.Core
open import Relation.Nullary.Negation
open import Relation.Binary.PropositionalEquality renaming ([_] to [_]ev)
open ≡-Reasoning

data Pal : List Char → Set where
    nil  :                                        Pal []

banacorn

var http = require('http');

var server = http.createServer(function (request, response) {
    response.writeHead(200, {"Content-Type": "text/plain"});
    response.write("Hello World\n");
    response.end();
});

server.listen(3000);

banacorn

module Bin where

--  `Set` is a reserved word in Agda, it's the type of all types
--  We are declaring that `Bin` is of type `Set`, `■` is of type `Bin`, and so on ...
data Bin : Set where
    ■   : Bin        -- 0
    0,_ : Bin → Bin  -- 2n
    1,_ : Bin → Bin  -- 2n+1

-- Binary number in a reversed order, for example

banacorn

Goal: show that TSP is NP-complete

• TSP is NP
• TSP is NP-Hard

TSP is NP

• Algorithm: given a tour, sum the weights, and see if it exceeds the bound
• The verifier runs in polynomial time

banacorn

Advenced Cache Performance Optimization

Optimization	Miss rate	Miss penalty	Hit time	Bandwidth	Note
compiler optmization	-
critical word first and early restart		-
merging write buffers		-
small & simple cache	+		-
way prediction			-