Skip to content

Grammars

A grammar is a 4-tuple \(G=\langle T,N,s,P\rangle\) where

  • \(T\) is a finite set of terminals
  • \(N\) is a finite set of non-terminals
  • \(s\in N\) is the starting symbol
  • \(P\subseteq (T\cup N)^*\times(T\cup N)^*\) s.t., \((u,v)\in P\Rightarrow\exists x\in N,\ell,r\in(T\cup N)^*:u=\ell xr\)

Regular Expressions

BNF like syntax

\(E:=0\vert 1\vert a\vert E+E\vert E\cdot E\vert E^*\)

\(\mathcal L:E\to 2^{A^*}\)

\(\mathcal L(0)-\emptyset\), \(\mathcal L(1)=\{\epsilon\}\), \(\mathcal L(a)=\{a\}\)

\(\mathcal L(E_1+E_2)=\mathcal L(E_1)\cup\mathcal L(E_2)\)

\(\mathcal L(E_1\cdot E_2)=\mathcal L(E_1)\cdot\mathcal L(E_2)=\{v,w\in A^*\vert v\in\mathcal L(E_1),w\in\mathcal L(E_2)\}\).

\(\mathcal L(E^*)=\mathcal L(E)^*=\cap_{n\geq 0}\mathcal L(E)^n\)

Term Algebra

A Signature \(\Sigma=(C,ar)\) where \(c=\{c_1,\cdots,c_n\}\) and \(ar:C\to w\).

\(ar\) is arity.

Term algebra on a signature \(\Sigma\) and a countable set \(V\) of variables is the smallest set \(Term_{\Sigma,V}\) s.t.,

  • \(V\subseteq Term_{\Sigma,V}\)
  • \(\forall c\in C,t_1,\cdots,t_{ar(t)}\in Term_{\Sigma,V}:c(t_1,\cdots,c_{ar(t)})\in Term_{\Sigma,V}\)

\(T_{\Sigma}=Term_{\Sigma,\emptyset}\subseteq Term_{\Sigma,V}\) is the set of closed terms.

Structural Induction

Given an inductively defined set, the structural induction principle can be used to prove properties on the elements of the set.

Principle of structural induction

To prove \(\forall t\in Term_{\Sigma,\emptyset}\)

Base case(s): Show \(p(c)\forall c\) s.t., \(ar(c)=0\)

Inductive step: Show \(p(t_1)\and\cdots\and p(t_k)\Rightarrow p(c(t_1,\cdots,t_k))\) for all \(c\) s.t. \(ar(c)=k>0\) and \(t_1,\cdots, t_k\in Term_{\Sigma,\emptyset}\).

What do we mean by correctness

Safety: Nothing bad happens

Liveness: Something good happens

Sequential programs can be though of as multi-threaded programs made of a single thread but

  • testing is hard with concurrency because of Heisenbugs. (poor reproducibility, failed tests hard help)
  • non-determinism is both a blessing and a curse

Modelling Behavior

\(Sys=(S,\to)\) where

  • \(S\) is a set of states
  • \(\to\subseteq S\times S\).

The evolution of a system can be described in terms of state transition

  • States represent the possible configurations the system can be in
  • Transitions represent the possible evolution from a given configuration

In its simplest form, such models can be mathematically rendered as binary relations.

\((s,s')\in\to\), usually written \(s\to s'\), reads "from state \(s\), \(Sys\) can evolve to \(s'\)"

\(Sys\) is deterministic if \(\forall s,s',s''\in S:s\to s'\or s\to s''\), we have \(s'=s''\)