In programs that somehow deal with context-free grammars automatically, we may want to check whether some part of the grammar “makes sense” and isn’t totally redundant and useless. In other words, we may want to check whether some non-terminal or production can come up in some arbitrary sentential form. This problem arises often when the program we are implementing accepts user-defined grammars. In this post, we will consider an existing algorithm that solves the problem as well as introduce and implement a new, more efficient algorithm that detects useless parts of an input grammar.

There exist different kinds of deductive systems in logic. Every deductive system consists of certain axioms and rules of inference. The problem of constructing a proof in every such system is quite difficult — computationally it is $\mathcal{NP}$-Hard, since satisfiability can be reduced to it. So it is a good idea to trade-off between logical axioms and inference rules. Hilbert (Frege)-style proof systems are interesting because most of them use several axioms but only one inference rule — modus ponens, unlike, for example, Gentzen natural deduction. In other words, Hilbert-style proof systems “push” all the complexity of constructing a proof into the axioms — it is hard to syntactically instantiate them, but once done it is easier to combine them as there is only one rule of inference — modus ponens. In this post, I will present a notation for these Hilbert-style proofs I came up with recently, that allows one to construct them in a more systematic way, with less “guessing”.

The SAT problem is the first problem proven to be $\mathcal{NP}$-Complete. However, many instances of this problem with certain properties can be solved efficiently in polynomial time. Well-known examples of such easy instances are 2-sat and horn formulas. All clauses in a 2-sat formula have at most 2 literals and horn-formulas consist only of clauses that contain at most one positive literal. In other words, a 2-sat clause is a conjunction of two implications and any horn clause can be rewritten as a conjunction of positive literals that implies either false or a negative literal. It may seem that satisfiability of formulas containing both 2-sat as well as horn clauses can be decided in polynomial time, however, because of the $\mathcal{NP}$-completeness that we will prove shortly, this is not the case unless $\mathcal{P} = \mathcal{NP}$. The problem also remains $\mathcal{NP}$-complete for Dual-horn clauses instead of normal horn clauses.

In linear algebra, orthogonal bases have many beautiful properties. For example, matrices consisting of orthogonal column vectors (a. k. a. orthogonal matrices) can be easily inverted by just transposing the matrix. Also, it is easier for example to project vectors on subspaces spanned by vectors that are orthogonal to each other. The Gram-Schmidt process is an important algorithm that allows us to convert an arbitrary basis to an orthogonal one spanning the same subspace. In this post, we will implement and visualize this algorithm in 3D with a popular Open-Source library manim.

In this post I will introduce an interesting connection between gray codes and the problem of minimizing propositional logic formulas in disjunctive normal forms (DNF’s). Both of these concepts are related to the Hamming distance between two binary sequences, which is the amount of bits that need to be flipped in one sequence in order to obtain the other one.

The dining philosophers problem is a well-known problem in computer science, originally formulated by Edsger Dijkstra to illustrate the possibility of deadlocks in programs where multiple threads lock and unlock multiple shared resources, such that a situation in which every thread is waiting for actions from other threads and no thread can thus continue it’s normal execution may occur. We will consider different approaches for solving this problem in the present post.

The singular matrix decomposition plays a major role in linear algebra and has a lot of applications, including lossy image compression. In this post we will discuss it in the context of the mentioned image compression with the focus on the intuition behind the algorithm, without going deep into the theory.

This post is about gray codes a.k.a. gray encoding of binary numbers. We will also cover some interesting properties, ideas and symmetries behind this encoding.

Almost every program has to somehow process and transform strings. Very often we want to identify some fixed pattern (substring) in the string, or, formally speaking, find an occurrence of $\beta := b_0b_1 \dots b_{n-1}$ in $\alpha := a_0a_1 \dots a_{m-1} \neq \varepsilon$. A naive algorithm would just traverse $\alpha$ and check if $\beta$ starts at the current character of $\alpha$. Unfortunately, this approach leads us to an algorithm with a complexity of $O(n \cdot m)$. In this post we will discuss a more efficient algorithm solving this problem - the Knuth-Morris-Pratt (KMP) algorithm.

Matrices are omnipresent in linear algebra. Columns of a matrix describe where the corresponding basis vectors land relative to the initial basis. All transformed vectors are linear combinations of transformed basis vectors which are the columns of the matrix, this is also called linearity. Algorithms that operate on matrices essentially just alter the way vectors get transformed, preserving some properties. Unfortunately, many algorithms are typically presented to students in a numerical fashion, without describing the whole graphical meaning. In this post we will first visualize simple linear transformations and then we will visualize Gaussian Elimination (with row swaps) steps as a sequence of linear transformations. To do this, we will use Python together with a popular Open-Source library manim.

Keep going!Keep going ×2!Give me more!Thank you, thank youFar too kind!Never gonna give me up?Never gonna let me down?Turn around and desert me!You're an addict!Son of a clapper!No wayGo back to work!This is getting out of handUnbelievablePREPOSTEROUSI N S A N I T YFEED ME A STRAY CAT