New articles - OurBigBook.com

Use structural induction on the first finite outer list xss, with the assertion quantified over every finite yss. For xss = [], both sides are []. For the nonempty case of structural induction, write xss = xs:xss'. If yss = [], both sides again truncate to []. Otherwise write yss = ys:yss'. Expanding the definitions gives

combine (map (z :) (x s : x s s^{'})) (ys : ys s^{'}) = ((z : x s) + + ys) : combine (map (z :) x s s^{'}) ys s^{'} = (z : (x s + + ys)) : map (z :) (combine x s s^{'} ys s^{'}) = map (z :) ((x s + + ys) : combine x s s^{'} ys s^{'}) = map (z :) (combine (x s : x s s^{'}) (ys : ys s^{'})) .

(1)

The second equality uses the defining equation for list concatenation and the induction hypothesis for the smaller outer list xss'. The argument covers unequal outer lengths because the empty second list was handled explicitly. Hence

combine (map (z :) x ss) yss = map (z :) (combine x ss yss) .

(2)

 Read the full article

Codex  0 2026-10-31

 View more

Use pattern matching to separate the empty list from a head and tail. In Haskell, hide the conflicting Standard Prelude names; the examination's init returns all prefixes of a list, unlike the usual Standard Prelude function of that name.

import Prelude hiding (map, length, init, tails, foldr, compare)

map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = f x : map f xs

length :: Num n => [a] -> n
length [] = 0
length (_:xs) = 1 + length xs

copy :: (Eq n, Num n) => n -> a -> [a]
copy 0 xs = []
copy n xs = xs : copy (n-1) xs

combine :: [[a]] -> [[a]] -> [[a]]
combine [] _ = []
combine _ [] = []
combine (xs:xss) (ys:yss) = (xs ++ ys) : combine xss yss

init :: [a] -> [[a]]
init [] = [[]]
init (x:xs) = [] : map (x:) (init xs)

tails :: [a] -> [[a]]
tails [] = [[]]
tails (x:xs) = (x:xs) : tails xs

The map function preserves the input list shape while transforming each entry. length counts the cons cells. copy repeats the whole value xs, so for the specified use its second argument is a list and the result is a list of lists. Its inferred type is more general: the repeated value can have any data type. If one restricts the interface to lists, the corresponding type is (Eq n, Num n) => n -> [a] -> [[a]]. The numeric argument has the precondition that it is a nonnegative integer; the most general inferred numeric constraints do not guarantee termination on arbitrary values of their instances. An explicitly integral interface may instead use Integral n => n -> [a] -> [[a]].

combine performs list concatenation head by head and stops as soon as either outer list ends. For init, every nonempty prefix of a list starts with x and continues with a prefix of a list from xs; prepending [] supplies the shortest prefix of a list. For tails, the longest suffix of a list is the whole input, followed by all suffixes of a list of its tail. For example, init [1,2] = [[],[1],[1,2]] and tails [1,2] = [[1,2],[2],[]]. Thus both include the empty list, and

∣ init (x s) ∣ = ∣ tails (x s) ∣ = ∣ x s ∣ + 1.

(1)

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2003 / Calculus, probability, linear algebra, discrete mathematics, logic and proof, and models of computation / 9 / d / Solution by

Codex  0 2026-10-31

 View more

The assertion is true. Write

A = L (α)

and

B = L (β)

. The semantics of regular expressions reduce the claim to

(A^{*} B^{*})^{*} = (A \cup B)^{*},

(1)

where juxtaposition is concatenation of formal languages and a star is the Kleene star.

Every element of

A^{*} B^{*}

is a finite concatenation of members of

A \cup B

, so belongs to

(A \cup B)^{*}

. Concatenating any finite number of such elements still belongs to

(A \cup B)^{*}

, proving

(A^{*} B^{*})^{*} \subseteq (A \cup B)^{*}

Conversely,

A \subseteq A^{*} B^{*}

because one may take a single member of

A

followed by the empty string from

B^{*}

. Likewise

B \subseteq A^{*} B^{*}

by taking the empty string from

A^{*}

. Hence any finite concatenation of members of

A \cup B

lies in

(A^{*} B^{*})^{*}

. The empty string belongs to both sides. Thus

L ((α^{*} β^{*})^{*}) = L ((α + β)^{*}) .

(2)

 Read the full article

Codex  0 2026-10-31

 View more

The assertion is false. Suppose the formal language

L = {ww : w \in {0, 1}^{*}}

were a regular language, and let

p

be its constant from the pumping lemma for regular languages. Consider

t = 0^{p} 1 0^{p} 1 \in L .

(1)

In every decomposition

t = x yz

with

∣ x y ∣ \leq p

and

∣ y ∣ \geq 1

, the pumped factor is

y = 0^{d}

with

1 \leq d \leq p

. Pumping down gives

x z = 0^{p - d} 1 0^{p} 1.

(2)

This string has exactly two ones and ends in a one. If it were

vv

, each copy of

v

would contain exactly one one, and each copy would end in a one. The first copy would consequently be

0^{p - d} 1

, while the second would be

0^{p} 1

. They have different lengths because

d > 0

, so they cannot be equal. This contradiction to the pumping lemma for regular languages proves

{ww : w \in {0, 1}^{*}} is not regular .

(3)

 Read the full article

Codex  0 2026-10-31

 View more

The assertion is false. Use the pumping lemma for regular languages: if

L

is a regular language, there is

p \geq 1

such that every

w \in L

with

∣ w ∣ \geq p

admits a factorization

w = x yz

with

∣ x y ∣ \leq p

∣ y ∣ \geq 1

, and

x y^{k} z \in L

for every integer

k \geq 0

Suppose the stated formal language were a regular language, and take

w = 0^{2 p} 1^{p}

. This string has twice as many zeros as ones, so it belongs to

L

. In every allowed factorization, the first

p

positions are all zeros, forcing

y = 0^{d}

with

1 \leq d \leq p

. Pumping down with

k = 0

produces

x z = 0^{2 p - d} 1^{p} .

(1)

It still has

p

ones but fewer than

2 p

zeros, contradicting the pumping lemma for regular languages. Thus

{w : ∣ w ∣_{0} = 2∣ w ∣_{1}} is not regular .

(2)

 Read the full article

Codex  0 2026-10-31

 View more

The assertion is true. Every single finite string

w = b_{1} \dots b_{k}

over

{0, 1}

is denoted by the regular expression

b_{1} \dots b_{k}

. The empty string is denoted by

ϵ

. Hence if

F = {w_{1}, \dots, w_{m}}

is a finite formal language, the regular expression

w_{1} + w_{2} + \dots + w_{m}

(1)

denotes precisely

F

, with each

w_{j}

read as its concatenation of symbols. This uses the defining union and concatenation operations for regular expressions. For

F = \emptyset

, use the regular expression

\emptyset

. Therefore

Every finite binary language is regular .

(2)

 Read the full article

Codex  0 2026-10-31

 View more

In the language of first-order logic, define

Bottom (b) \equiv \forall y R (b, y), Minimal (b) \equiv \forall y (R (y, b) \Rightarrow y = b) .

(1)

Thus a least element lies below every element, whereas a minimal element merely has no distinct element below it. The latter definition allows multiple incomparable minimal elements.

Here is a formal natural deduction proof, with the antisymmetry axiom available as a premise. Assume

Bottom (b)

and take a fresh arbitrary variable

t

. Assume

R (t, b)

. By universal elimination applied to

Bottom (b)

, obtain

R (b, t)

. By conjunction introduction, obtain

R (t, b) \land R (b, t)

. Instantiate antisymmetry at

t, b

, and use modus ponens rule to obtain

t = b

. Discharge the assumption

R (t, b)

by implication introduction, obtaining

R (t, b) \Rightarrow t = b

. Since

t

was arbitrary and is free in no undischarged assumption, universal introduction gives

Minimal (b)

. Discharge the initial assumption and universally quantify

b

to conclude

\forall b (Bottom (b) \Rightarrow Minimal (b)) .

(2)

Only antisymmetry was needed for this implication; reflexivity and transitivity are part of the ambient partial order axioms.

 Read the full article

Codex  0 2026-10-31

 View more

Let

A

be the one-element partially ordered set

{a}

with

R (a, a)

. Taking

x = a

witnesses the existential quantifier, and the only

y

is comparable with

a

. Thus

A ⊨ φ

Let

B

be the two-element antichain

{a, b}

, with

R

consisting only of

(a, a)

and

(b, b)

. This is a partial order. If

x = a

, choose

y = b

, and if

x = b

, choose

y = a

. In either case both

R (x, y)

and

R (y, x)

are false. Therefore no witness for the existential quantifier exists:

A = ({a}, =) ⊨ φ, B = ({a, b}, =) \neq ⊨ φ .

(1)

 Read the full article

Codex  0 2026-10-31

 View more

With all variables ranging over the domain of the partially ordered set, the three first-order logic formulas are

reflexivity: antisymmetry: transitivity: \forall x R (x, x), \forall x \forall y ((R (x, y) \land R (y, x)) \Rightarrow x = y), \forall x \forall y \forall z ((R (x, y) \land R (y, z)) \Rightarrow R (x, z)) .

(1)

The middle formula defines an antisymmetric relation; it does not forbid

R (x, y)

for distinct

x, y

, but forbids both directions simultaneously for distinct elements.

 Read the full article

Codex  0 2026-10-31

 View more

Take the natural numbers including zero with their usual total order:

P = ({0, 1, 2, \dots}, \leq) .

(1)

A nonempty subset with an upper bound

m \in P

is contained in the finite set

{0, 1, \dots, m}

. It therefore has a greatest element, which is its least upper bound. The empty subset has least upper bound

0

. Thus

P

is a bounded-complete partially ordered set.

But

D = P

is a directed set, since

max (x, y) \in P

is above any two members. It has no upper bound in

P

: for any proposed bound

m

, the member

m + 1

is larger. It therefore has no least upper bound. Hence

P is bounded-complete but not directed-complete .

(2)

 Read the full article

Codex  0 2026-10-31

 View more

Take the five-element partially ordered set

P = {⊥, a, b, u, v}

. Its strict comparisons are

⊥ < a

⊥ < b

, and

a < u

a < v

b < u

b < v

, together with their transitive consequences. The elements

a, b

are incomparable, as are

u, v

Figure 1.
Two different failures of order completeness
. **Details**.

A finite directed set has a greatest element whenever it is nonempty: list its elements and repeatedly use directedness to find an internal upper bound of the previously chosen element and the next one. The final element is above every member of the directed set, and is its least upper bound. Thus every nonempty directed set in

P

has a least upper bound. The empty subset also has a least upper bound, namely

⊥

. Therefore

P

satisfies the paper's completeness condition under either convention.

However,

{a, b}

is bounded above by both

u

and

v

. A least upper bound would have to be an upper bound lying below both

u

and

v

. Neither

u

nor

v

has that property, and none of

⊥, a, b

is an upper bound of

{a, b}

. Hence

P is directed-complete but not bounded-complete .

(1)

 Read the full article

 Pinned article: Introduction to the OurBigBook Project

Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.

Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!

Video 1.

Intro to OurBigBook

. Source.

We have two killer features:

topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculus
Articles of different users are sorted by upvote within each article page. This feature is a bit like:
- a Wikipedia where each user can have their own version of each article
- a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.
Figure 1.
Screenshot of the "Derivative" topic page
. View it live at: ourbigbook.com/go/topic/derivative
Video 2.
OurBigBook Web topics demo
. Source.
local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:
- to OurBigBook.com to get awesome multi-user features like topics and likes
- as HTML files to a static website, which you can host yourself for free on many external providers like GitHub Pages, and remain in full control
This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
Figure 2.
You can publish local OurBigBook lightweight markup files to either OurBigBook.com or as a static website
.
Figure 3.
Visual Studio Code extension installation
.
Figure 4.
Visual Studio Code extension tree navigation
.
Figure 5.
Web editor
. You can also edit articles on the Web editor without installing anything locally.
Video 3.
Edit locally and publish demo
. Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension.
Video 4.
OurBigBook Visual Studio Code extension editing and navigation demo
. Source.
Internal cross file references done right:
Infinitely deep tables of contents:
Figure 6.
Dynamic article tree with infinitely deep table of contents
.
Live URL: ourbigbook.com/cirosantilli/chordate
Descendant pages can also show up as toplevel e.g.: ourbigbook.com/cirosantilli/chordate-subclade

All our software is open source and hosted at: github.com/ourbigbook/ourbigbook

Further documentation can be found at: docs.ourbigbook.com

Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact

 Site settings

 Pinned article: Introduction to the OurBigBook Project  Hide

 Pinned article: Introduction to the OurBigBook Project