In the honor of my two esteemed colleagues (@abiteboul.com and Victor Vianu), the Abiteboul–Vianu theorem is now formalized and machine-proofed as part of my descriptive-complexity Lean 4 library.
pierresenellart.github.io/descriptive-...
![theorem DescriptiveComplexity.ifpDefinableFree_eq_pfpDefinableFree_iff_ptime_eq_pspace :
(∀ {L : FirstOrder.Language} [inst : L.IsRelational] (P : DecisionProblem L), IFPDefinableFree P ↔ PFPDefinableFree P) ↔ PTIME = PSPACE
The Abiteboul–Vianu theorem. The inflationary and partial fixed-point logics have the same expressive power on unordered finite structures exactly when polynomial time and polynomial space coincide.](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:fhv65kba5do4hgyf7yq4dtyo/bafkreifwpbn737bae4amsnmmns45sfqgsc6z22d3p7eaycq4adgtpsdf7u)
Pierre Senellart
@pierre.senellart.com
173 followers 64 following 115 posts
Professor of computer science at ENS-PSL @normalesup.bsky.social, head of Inria Valda team. VP Digital infrastructure and IT convergence, PSL University @psl-univ.bsky.social.
![Screenshot of the README
# utool — simple Unicode operations in command-line
utool is a command-line tool to perform simple Unicode operations on text
streams.
## Usage
```
utool [filters] [input]
```
utool follows the standard Unix convention: input from files given as
argument or from standard input, output to standard output.
The filters are applied in the order they are given.
The character encoding is determined by the `LC_CTYPE` locale cateogry.
## Filters
### `--lowercase`
Convert to lowercase.
### `--uppercase`
Convert to uppercase.
### `--nfd`
Convert to Normalization Form D (decomposed), i.e. convert codepoints
corresponding to characters with diacritics into a base codepoint and the
diacritics as combining codepoint.
### `--nfd`
Convert to Normalization Form C (composed), i.e. merge combining codepoints
with the base codepoint if possible.
### `--nfkd`
Convert to Normalization Form KD (compatibility decomposed).
### `--nfkd`
Convert to Normalization Form C (compatibility composed).
### `--decomb` or `--remove-combining`
Remove combining codepoints. Useful along with `--nfd` to remove diacritics.
### `--char-names`
Replace each char by its official name, each on a line.](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:jvdcbjy7idsnku5utkw7ikn4/bafkreiafhh63ngbnzwqkp67rliasaegb6mlldjmey4q7zkojvedr75dz7y)
