Monday, 22 July 2013

[English Writing] commas (,) usage

Basic Rules

For more, please refer to grammarbook.com

R1. Dependent clause + Main clause

When starting a sentence with a weak clause, use a comma after it. Conversely, do not use a comma when the sentence starts with a strong clause followed by a weak clause. (from grammarbook.com)
Examples:
  • If I ever complete my PhD successfully, I will be amazed.
    • I will be amazed if I ever complete my PhD successfully.
  • When I use it, the e-mail always breaks down.
    • The e-mail always breaks down when I use it.

R2. Adverbs that relate to the whole sentences

Examples:
  • However, some researches adopt a markedly different approach.
  • Superisingly, he did not go to the school yesterday.

R3. Speech + comment

Examples:
  • "Paul Klee," he remarked, "was the first person to acutally paint commas".

R4. When a sentence is 'broken open' in the middle

Examples:
  • Some researches, on the other hand, adopt a different approach.
  • There are, it seems, two different solutions to the enthanasia problem.

R5. Items in lists

Use commas to separate words and word groups with a series of three or more.
Examples:
  • Many essays are over-long, convoluted and boring. [UK]
  • Many essays are over-long, convoluted, and boring. [US]
  • Do not steal, copy, or plagiarise ideas.

R6. Separate two adjectives when end can be inserted between them

Examples:
  • He is a strong, healthy man.
    • He is a strong and healthy man.
  • He is a lonely, young boy.

R7. Separate day and month from the year when writing date.

Examples:
  • I will have a business travel from May 15th, 2011.
  • I will have a business travel from May 2011. (If day, month or year is ommitted, no comma)

[English Writing] hyphen and dashes

Three types of dashes and its corresponding Latex within parentheses

  • Hyphen - (-)
  • en dash – (--)
  • em dash — (---)

Hyphen - (-)

A short horizontal mark of punctuation ( - ) used between the parts of a compound word or name or between the syllables of a word when divided at the end of a line. (from About)
Examples:
  • concatenation of compount words, e.g. eight-year-old
  • on-site support
  • follow-up

en dash – (--)

  • An en dash, roughly the width of an n, is a little longer than a hyphen. It is used for periods of time when you might otherwise use to. (from grammarbook)
  • An en dash is also used in place of a hyphen when combining open compounds.
    • attaches a prefix or suffix to an unhyphenated compound
Examples:
  • section 3–5
  • post–World War I treaty
  • New York–based writer

em dash — (---)

A mark of punctuation (—), technically known as an em dash, used to set off a word or phrase after an independent clause or to set off words, phrases, or clauses that interrupt a sentence. (from About)
"A dash is a mark of separation stronger than a comma, less formal than a colon, and more relaxed than parentheses." (William Strunk, Jr, and E.B. White, The Elements of Style)

Set Off Words or Phrases After an Independent Clause

"Life, said Samuel Butler, is like giving a concert on the violin while learning to play the instrument—that, friends, is real wisdom." (Saul Bellow, "My Paris," 1983)
"By trying we can easily learn to endure adversity—another man's, I mean." (Mark Twain)

Dashes Used to Set Off Words or Phrases That Interrupt a Sentence

Then, a review of model checking approaches—refinement based and temporal logic based—for currently applicable tools is taken, which provides the insight into the appropriate approaches for Circus and CML
"Copper Lincoln cents—pale zinc-coated steel for a year in the war—figure in my earliest impressions of money." (John Updike, "A Sense of Change." The New Yorker, Apr. 26, 1999)

Friday, 19 July 2013

Reference numbering in Latex

Problems

Multiple references may cause a very weird problem.
For example, some time this VDM [2][1] is gotten from the LaTeX \cite{vdm2001} \cite{vdm1999}.
The order in reference is not correct. The right order will not depend on which citation is placed first and it should depend on which reference is referred first.

Solution 1

Use the cite package
\usepackage{cite} \cite{vdm2001, vdm1999}
This will result in VDM [1,2]

Solution 2

Use the natbib package with options
\usepackage[sort&compress]{natbib}
  • \citet for textual citations
  • \citep for parenthetical citations
For example
  • \citet{vdm2001}
  • \citep{vdm2001}
  • \citet[p.~20]{vdm2001}
  • \citet[chap.~2]{vdm2001}
  • \citet{vdm2001,vdm1999}

Thursday, 11 July 2013

R: basics - installastion, environment and debug

Install R

  • $sudo apt-get install r-base

R edit environment

R basics

  • Install extra package
    • > install.packages("ismev")
  • Source R script
    • > source("fit-gumbel.r")
  • Call function provided by fit-gumbel.r
    • > fit-gumbel("in.dat")

R debug

take optim function as an example

  • display source code of optim
    • > edit(optim)
  • set debug mode
    • > debug(optim)
  • check debug mode
    • > isdebugged(optim)
  • cancel debug mode
    • > undebug(optim)
  • debug optim (R source code src/library/stats/R/optim.R)
    • > debug(optim)
    • > out <- gumbel(dat)
    • Browser[2]> where
    • Browser[2]> [RET] - next step
    • Browser[2]> c - continue
    • Browser[2]> n
    • Browser[2]> Q
    • Browser[2]>

tmux usage

  • tmux quick set
    • tmux to take out the tmux terminal environment
    • C-b % to split window into two panes (vertically)
    • C-b :split-window to split window into two panes (horizontally)
    • C-b o switch to next pane
    • C-b x kill current pane
  • C-b has change to C-a
    • download a tmux.conf file
    • tmux source-file /devt/dev-rye/tmux-conf/tmux.conf
    • C-a | split vertically
    • C-a - split horizontally

Friday, 14 June 2013

Author name is 3em dash when using bibtex file to output bibliography in Latex

Problems

Entry in .bib file (edit by Jabref)

@INBOOK{Baier2008a,
  chapter = {4},
  pages = {170-198},
  title = {{P}rinciples of model checking},
  publisher = {MIT Press},
  year = {2008},
  author = {Christel Baier and Joost-Pieter Katoen},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  isbn = {978-0-262-02649-9},
  owner = {randall},
  timestamp = {2013.05.23}
}
The output will be like that:

[22] ——, Principles of model checking. MIT Press, 2008, ch. 4, pp. 170–198.

Try
If I remove the hyphen which is used to connect the name, it will be alright.

@INBOOK{Baier2008a,
  chapter = {4},
  pages = {170-198},
  title = {{P}rinciples of model checking},
  publisher = {MIT Press},
  year = {2008},
  author = {Christel Baier and Joost-Pieter Katoen},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  isbn = {978-0-262-02649-9},
  owner = {randall},
  timestamp = {2013.05.23}
}
The output will be like that:

[22] C. Baier and J. P. Katoen, Principles of model checking. MIT Press, 2008,
ch. 4, pp. 170–198.
However, the similar entry 
@BOOK{Baier2008,
  title = {{P}rinciples of model checking},
  publisher = {MIT Press},
  year = {2008},
  author = {Christel Baier and Joost-Pieter Katoen},
  pages = {I-XVII, 1-975},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  isbn = {978-0-262-02649-9},
  owner = {randall},
  timestamp = {2013.05.23}
}
will give the right output
[21] C. Baier and J.-P. Katoen, Principles of model checking. MIT Press, 2008.

Root Cause
If two entries in .bib file have the same author name, then one of them will become 3em dash (——).
It's default behaviour defined in IEEEtran.bst style. 


To remove this limitation, change the CTLdash_repeated_names value to no in .bib file
@IEEEtranBSTCTL{IEEEexample:BSTcontrol,
  CTLdash_repeated_names = "no"
}
Then add the following line in the tex file
\bstctlcite{IEEEexample:BSTcontrol}
However,  if the documentclass is not IEEEtrans, then this command \bstctlcite is not available. So this try will failed too.

Solution:
For the Latex file which has documentclass IEEEtrans, the above solution may be applied. For others (Article and Book class), just leave (——), it's not an error
   

"LaTeX Error: Too many math alphabets used in version czt"

This error means you have used more than 16 math symbol fonts (latex limitation).

Solution 1:  (http://valis.cs.uiuc.edu/blog/?cat=37)
Bypass this limit by specifying the only used font, e.g.
$\text{\usefont{U}{bbm}{m}{n}{H}}$ 

 Solution 2: (Work for this case)
 Replace the txfonts package with mathtools
Or remove the txfonts package if you don't need it
%\usepackage{txfonts} %\varparallel
 \usepackage{mathtools}

Solution 3:
too many math alphabets in version normal
\usepackage{amssymb}
\newcommand\hmmax{0} % default 3
 % \newcommand\bmmax{0} % default 4
 \usepackage{bm}

Monday, 3 June 2013

Substitution, Unification and Term Rewriting

Unification is the basis of term rewriting system, and unification algorithms is the heart of the computation model of logic programs.

Term:
terms are expressions which can be obtained from constant symbols, variables and function symbols. Constant symbols are the 0-ary functions, so no special syntactic class is needed for them.
  • Function symbols: one that has no other property than its name and arity
  • Terms that do not contain free variables are known as ground terms
  • A ground term of a formal system is a term that does not contain any free variables;
  • free variable: y is free variable in \( \forall x \in X \bullet (x+y) > 0 \)
  • bound variable: x is bound variable in \( \forall x \in X \bullet (x+y) > 0 \)
  • Hence \( \forall x \in X \bullet (x+y) > 0 \) is not a ground term, but \( \forall x \in X \bullet x > 0 \) is a ground term
  • x and y are variables, and f is a binary function symbol, then \( f(x,y) \) is a term
Arity - the number of arguments or operands the functions or operation accepts. For example, the arity of \( f(x)=x+1 \) is 1; the arity of \( f = 3 \) is 0; the arity of \( f(x,y,z) = x + y + z \) is 3.
  • 0-ary function or operation: (arity == 0) constant symbols
  • unary function or operation: (arity == 1) such as \( f(x) = x * 2 \), (unary operator) \( -x \)
  • binary function or operation: (arity == 2) such as \( f(x,y) = x + y \)
  • ternary function or operation: (arity == 3)
Signature:
A signature \( \Sigma \) is a set of function symbols, where each \( f \in \Sigma \) is associated with a non-negative integer n, the arity of \( f \). \( \Sigma^{0} \) denotes a set of constant symbols, while \( \Sigma^{n} \) denotes a set of n-ary function symbols.
  • For example, group \( \Sigma_G := \{e, i, f \} \) where e is 0-ary, i is 1-ary, and f is 2-ary
  • For example, a set of non-negative integers. e for smallest non-negative integer, i denotes the successor function \( succ(x) = x + 1 \), and f denotes the addition function \( f(x,y) = x + y \)
Substitution:
Substitution is a syntactic transformation on strings of symbols of a formal language
  • a substitution is a finite set of the form $$ \theta =  \{v_1 \mapsto t_1, ..., v_n \mapsto t_n \}$$, where 
    • \(v_i\): distinct variables; 
    • \( t_i \): terms with \(t_i \ne v_i\);
    • \( v_i \mapsto t_i \): binding
  • Substitution application:  \( E \theta \)
    • E - expression
    • \(\theta\) - substitution
    • Simultaneously replacing each occurrence of \(v_i\) in E with \(t_i\)
    • For example, \(E = p(x,y,f(a))\), \(\theta = \{x \mapsto b, y \mapsto x\}\), \(E \theta = p(b,x,f(a))\).
  • Substitution Composition
    • Two substitutions:  $$ \theta =  \{v_1 \mapsto t_1, ..., v_n \mapsto t_n \}$$ $$ \sigma =  \{u_1 \mapsto s_1, ..., u_n \mapsto s_n \}$$ $$\theta \sigma =  \{v_1 \mapsto t_1 \sigma, ..., v_n \mapsto t_n \sigma,  u_1 \mapsto s_1, ..., u_n \mapsto s_n\}$$
    • For example, \( \theta = \{x \mapsto f(y), y \mapsto z\} \), \( \sigma = \{x \mapsto a, y \mapsto b, z \mapsto y\}\), \( \theta \sigma = \{x \mapsto f(b), z \mapsto y\} \)
  • Empty Substitution \( \varepsilon \)
  • Renaming substitution
    • \( \theta =  \{x_1 \mapsto y_1, ..., x_n \mapsto y_n \} \) is a renaming substitution if \(y_i \) are distinct variables
  • More general substitution (MGS)
    • a substitution \(\theta\) is more general than a substitution \( \sigma \), written \(\theta \leq \sigma \), iff there exists a substitution \(\lambda\) that $$ \theta \lambda = \sigma $$
Abstract Reduction System:
  • An abstract reduction system is a pair \( (A, \to) \), where the reduction \( \to \) is a binary relation on the set A, i.e. \( \to \subseteq A \times A \). Written \(a \to b \), instead of \( (a,b) \in \to \)
  • Program evaluation: \(a0 \to a1 \to ... \). Starting from the initial program a0, and try to reach a normal formal
  • Normal formal is the program which can not be reducible
  • Let \(\Sigma\) be a signature and \(V\) a countably infinite set of variables disjoint from \(\Sigma\). A \(\Sigma\)-identity is a pair \((s,t) \in T(\Sigma, V) \times T(\Sigma, V)\). Identities will be written as \(s \approx t\)
  • reduction relation \( \to_E \), where E is a set of \(\Sigma\)-identity
Unification:
Unification, in computer science and logic, is an algorithmic process by which one attempts to solve the satisfiability problem. The goal of unification is to find a substitution which demonstrates that two seemingly different terms are in fact either identical or just equal. Unification is widely used in automated reasoning, logic programming and programming language type system implementation
  • Unification is the process of solving the satisfiability problem: given \(E\), \(s\) and \(t\), find a substitution \(\theta\) such that \(\theta s \approx_E \theta t\)
  • For special case, where \(E=\emptyset \), this case of unification is called syntactic unification, because the unification aims to find a \(\theta\) such that \(\theta s = \theta t\) i.e. \(\theta s\) and \( \theta t\) are syntactically identical.
  • If \(E \neq \emptyset \), this is referred to semantic unification
  • Unifier of Expressions: a substitution \(\theta\) is a unifier of expressions E and F iff $$\theta E = \theta F$$
    • For example, \(E = f(x,b,g(z)), F = f(f(y),y,g(u))\). Then \( \theta = \{x \mapsto f(b), y \mapsto b, z \mapsto u\}\) is a unifier of E and F since $$\theta E = f(f(b),b,g(u))$$ $$\theta F = f(f(b),b,g(u))$$
  • Unifier is a solution to the equation by substitution. Find a substitution to make two expressions E and F are equal and this substitution is a solution to this equation, named unifier.
Unification in Prolog:

Unification in Perl: