banacorn

import sys
from M2Crypto import RSA
if len(sys.argv) < 3:
    print "Please input public key and data"
    sys.exit()

rsa=RSA.load_pub_key(sys.argv[1])
fname = sys.argv[2]
file = open(fname, 'r')
data = file.read()

banacorn

scan :: String -> Pipeline [Token]
scan str = go (alexStartPos, '\n', [], str)
    where
        go inp@(pos, _, _, str) = case alexScan inp 0 of
            AlexEOF -> return []
            AlexError (pos, _, _, _) -> throwError $ LexError (toPosition pos) "fucked up"
            AlexSkip  inp_ len     -> go inp_
            AlexToken inp_ len act -> do
                xs <- go inp_
                return $ act pos (take len str) : xs

banacorn

• Leaf: a vertex of degree 1.
• Tree-graphic: a sequence is said to be tree-graphic if it is a permutation of the degree sequence of a tree.

3.1.1

Every tree with at least 1 edge hase at least 2 leaves.

3.1.2

If the degree of every vertex of a graph is at least 2, then that graph must contain a cycle.

banacorn

Chapter 2: Structure and Representation

• **Preserves Adjacency **, Preserves Non-adjacency: homomorphisms that preserve these properties.
• Structure-preserving of Simple Graph: preserves both adjacency and non-adjacency, i.e. adjacent u v <=> adjacent h(u) h(v)
• Isomorphism of Simple Graph: the bijection that is structure-preserving
• Structure-preserving of Graph: preserves the number of edges between every pair of vertices.
• Isomorphism of Graph: the bijection that is structure-preserving
• Consistent: For graph G and H, a pair of bijections (vertex and edge) is consistent if for all egde in G, the isomorphism maps its endpoints.
• The Möbius Ladder: denoted MLₙ, obtained by cross-match one pair of its parallel egdes.
• Isomorphism Type: the equivalent class under graph isomorphism.

banacorn

Chapter 1: Introduction to Graph Models

• Graph, Vertices, Edges, Endpoints
• Join, Neighbor
• The Open Neighborhood of a vertex v in a graph G, denoted N(v), is the set of all neighbors of v.
• The Closed Neighborhood of a vertex v in a graph G, denoted N[v], is the set of all neighbors of v and itself.
• Proper Edge: joins two distinct vertices.
• Self-loop: joins a single endpoint to itself.
• Multi-edge: A collection of tow or more egdes having identical endpoints.
• Edge Multiplicity: the number of egdes within the multi-edge.

banacorn

{-# LANGUAGE OverloadedStrings #-}

import              Data.Attoparsec.Text
import              Data.Text (Text)
import qualified    Data.Text as T
import              Prelude   hiding (take)

input :: Text
input = "𝟘a"

banacorn

 {-# LANGUAGE OverloadedStrings #-}

import Control.Concurrent
import Data.ByteString (ByteString, empty)
import Data.ByteString.Char8 (pack, unpack)
import System.Environment (getArgs)
import System.IO (openFile, IOMode(..))
import System.IO.Streams
import System.Console.ANSI
import Prelude hiding (read)

banacorn

                    _oo0oo_
                   o8888888o
                   88" . "88
                   (| -_- |)
                   0\  =  /0
                  __/`---'\__
               .' \\|     |// '.

banacorn

Mac OS X 的 Agda 安裝指南

詳細可以看看這裡 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.MacOSX

透過 Hackage 安裝（難度 ✮✮☆☆☆）

1. 首先把 64bit 的 Haskell Platform 裝好 http://www.haskell.org/platform/

2. 把這份 script 複製到 /usr/bin 並且執行它 http://www.haskell.org/platform/ghc-clang-wrapper

banacorn

Semantics

Lecture 1

• p. 11: For every three terms M0, M1, and M2 => For every three terms M1, M2, and M3

Type Theory & Logic

Lecture 2