Theory of computation

General

Kleene's theorem: establishes equivalence between FA and regular languages
Regular languages: aka rational languages

A 2-stack DPDA is as powerful as a deterministic TM. ²
aⁿcbⁿ is a CFL but not regular.
aⁿbⁿcⁿ is neither a CFL nor a regular language.
Total Turing machine: A TM that always halts.
- ie, for any input.
- Represents a total function that finishes.
Medvedev machine:
- An FSM where output is the current state
- There is no separate output logic
- Like a restricted form of Moore machine
- https://www.vhdl-online.de/courses/system_design/synthesis/finite_state_machines_and_vhdl/medvedev

Turing machine

One-tape turing machine is a 7-tuple:

M = (Q, Γ, b, Σ, δ, q₀, F)

Q: set of states
Γ: Tape alphabet.
- The set of symbols that can show up in the tape
b: blank symbol.
- b∈Γ
Σ: input alphabet
- Σ ⊆ (Γ \ {b})
δ: transition function
- δ:
q₀: initial state
F: set of final states

DPDA vs NPDA

Unlike in the case of finite automata, DPDA are NPDA are not equivalent.

For example, wwᴿ can be accepted by a NPDA but no DPDA can handle it.

∵ the time to switch from the 'w-mode' to the 'wᴿ-mode' cannot be figured out deterministically since there is no delimiter. The possiblity always has to be explored.

wcwᴿ can be handled by DPDA if c ∉ w.

Halting problem

Problem: For a specific input, will the Turing machine halt (ie, finish computing and give a result)?

For a given word and a Turing machine, there is no way to definitely tell whether the Turing machine will aceept that word (ie, halt) or not.

From Sipser:

recognizers are more powerful than deciders

Universal Turing machine

A TM capable of simulating any TM.

Pumping lemma for regular languages

Can be used to show that a language is not regular.
Can't be used to show that a language is regular.

The lemma:

L: the language
s: a string of L

∃n∈ℕ such that for any s ∈ L:

|s| ≥ n
s = xyz
- |y| > 0
- |xy| ≤ n

Then,

∀i≥0, xyⁱz ∈ L

if L is regular.

Proof (informal):

Let

M be the DFA accepting string of L
n be the number of states of M
s ∈ L such that |s| ≥ n

From: https://www2.lawrence.edu/fast/GREGGJ/CMSC515/chapt01/Pumping.html

Context free languages

An example CFL: aⁿbⁿ where n≥0.

CFG:

S -> aSb | ε

if only n>0 is allowed, the grammar could be like:

S -> aSb | ab

—

If w ∈ {a,b},

wcwᴿ is a CFL:

S -> aSa | bSb | c

but wcw is not a CFL.

∵ the stack can only be popped in last-in-first-out order. wcw requires FIFO order.

—

aⁿbⁿcᵐ where n≥0, m≥0 is a D-CFL.

S = IE
I = aIb | ε
E = cE | ε

Master's theorem

Expressed as a recurrence relation.

A task of size n can be divided into k sub-tasks each of size n/b.

The results of these sub-tasks are then combined in 𝑂(nᵈ) time to get the final result.

T(n) = k.T(n/b) + 𝑂(nᵈ)

Properties of languages

From here:

	RL	DCFL	NCFL	CSL
Union	Y	N	Y
Complement	Y⁶	N	N	Y
Intersection	Y	N ?	N ?
Concatentation	Y
Kleene star	Y

Star free languages

Reference: https://www.irif.fr/~jep/PDF/MPRI/MPRI.pdf

Given:

Σ: finite alphabet

then set L of star-free languges within Σ* is the smallest set such that:

∅ ∈ L	Includes empty language
{ε} ∈ L	Includes language with only empty word
(a ∈ Σ) -> {a} ∈ L	ie, a uni-symbol word language

and is closed under

finite union
finite product/concatentation
complementation (this one is unlike normal regex)

Examples:

Σ* is star free.
- Σ* = ∅ᶜ

Doubts:

Star free languages over Σ ⊆ languages over Σ

I guess this type in coq can represent star-free languages over Σ:

Inductive t (Σ: Type): Type :=
| Nul: t Σ
| Nil: t Σ
| Char: Σ -> t Σ
| Cat: t Σ -> t Σ -> t Σ
| Alt: t Σ -> t Σ -> t Σ
| Cmp: t Σ -> t Σ.

Kamp's theorem: LTL properties are equivalent to star-free languages

LTL	Star-free
¬p	pᶜ
p ∨ q	p + q
X p	true; p
p U q	p*;q

a* is star free for any finite alphabet. a* being same as (Σ* \ a*)

https://cs.stackexchange.com/questions/10768/star-free-language-vs-regular-language

Σ* = ∅ᶜ

a* = (Σ* (Σ \ a) Σ*)ᶜ
   = (∅ᶜ (Σ \ a) ∅ᶜ)ᶜ

—

LTL:

p := prop
   | ¬p
   | p ∨ p
   | X p
   | p U p


G p = p U ⊥

Linear Temporal Logic (LTL)

Symbol	Description
b	Boolean expression
¬ p	Not
X p	Next
p ∨ q	Or
p U q	Until (strong)

Derived operations:

Symbol	Description
G p	Global
F p	Finally
p ∧ q	Or
p M q	Release (strong)

Past-time LTL (pLTL)

Has:

Symbol	Description
`p S q`	since
`P p`	previously

PLTL is as expressive as LTL but properties can be much more succinct.

p S q is like q+p.* (or in PSL style, q+p[*]).

https://people.irisa.fr/Nicolas.Markey/PDF/MyPapers/eatcs-bull79()-Mar.pdf

Metric TL (MTL)

Has interval for U and F in LTL.