All algebraic data types are enumerable, so I want to assign a natural number to any algebraic data type. And then I want to assign a natural number to every instance of that type.

So I need bijection.


I want to start series of posts about design and implementation curve editor, like this one from Gimp software:

image

With Typescript and React. Let's start!


Concept of discrete world

  1. There is finite discrete world
  2. World consists from objects
  3. Every object is atomic or contains other objects
  4. Every object is unique, that means:
  5. No one part of object is shared with some other object
  6. No object or its part contains itself (also in transitive manner)
  7. World exists finite amount of time
  8. Time consists from discrete clock ticks
  9. Something could happen only at some clock tick
  10. 'Something' is world state change: one object or one from its parts are created or removed

System concept

  1. System consists from two parts: world and computer
  2. Computer have fixed collection of laws describing possible state transitions
  3. Laws are permitting only one transition per tick
  4. World state change is happening only when laws are not violated.

Laws language

  1. Rules that describe initial world state
  2. Rules that describe state transitions
  3. Every object have a reason to exist: by rule application or as a part of an initial state

The code

$$ \frac{n!}{k!(n-k)!} = \binom{n}{k} $$

is rendered as the formula

n!k!(nk)!=(nk)\frac{n!}{k!(n-k)!} = \binom{n}{k}


I want to enumerate given finite class of abstract objects.


Want to refresh my knowledge about Prolog. I am curious about is it possible to use Prolog for context-free string parsing? This task could help me to understand differences between Prolog and SMT solvers. I already implemented parser with Z3, I want to do the same with Prolog.