i2lang.org Open in urlscan Pro
46.23.81.157  Public Scan

Form analysis
0 forms found in the DOM

Text Content

I2: A LANGUAGE FOR VERIFIED REASONING

i2 is a language designed to make formal verification easy. While there has been
great progress in this area in recent years, in most cases, formal verification
remains an arcane art inaccessible to "the unitiated". We hope to change this by
presenting a small, orthogonal feature set in a simple syntax that can be
learned in an afternoon.

Beneath is the first theorem Landau derives from the Peano axioms:

tmpl thm1(m nat, n nat) { !eq(m, n) ==> !eq(succ(m), succ(n)) } {
	eq(succ(m), succ(n))
==> { injectivity(m, n) }
	eq(m, n);
};

That is, for all natural numbers m,nm, nm,n we have (m≠n)  ⟹  (succ(m)≠succ(n)).
(m \ne n) \implies (\text{succ}(m) \ne \text{succ}(n)).
(m=n)⟹(succ(m)=succ(n)). However, the above code will not verify on its own,
since it makes reference to many undefined objects. The axioms that power it are
as follows:

/* eq: Equality. i2 currently supports only logical operators and funtional
 * application, because we haven't yet found a simple way of introducing
 * higher-order operators (such as the equals-sign). */
@func eq(x any, y any) bool;

/* nat: A natural number. */
@func nat(x any) bool;

/* Types and predicates are the same thing in i2: boolean-valued functions.
 * However, we do permit the syntax
 * 	x P
 * to indicate "x is of type P", i.e. that P(x) is true.
 * The `@' means "axiomatic": we are merely postulating the existence of the 
 * types rather than providing an expression to which it evaluates. */

/* 1 is a natural number. */
term 1 nat;

/* This is like a global constant declaration. It occupies the place of Peano's
 * first axiom that 1 ∈ N. */

/* succ: For each x there exists exactly one natural number, called the
 * successor of x. */
@func succ(x nat) nat;

/* In other words: we postulate the existence of the succ(x) for every natural
 * number x. */

/* injectivity: If succ(x) == succ(y) then x == y. */ 
@tmpl injectivity(x nat, y nat) { eq(succ(x), succ(y)) ==> eq(x, y) };

/* The `@' here now indicates that the statement given in the template is
 * axiomatic (to be accepted by the verifier without proof). */

With three additional axioms, we are in a position to make our first inductive
proof.

/* succ_notone: We always have succ(x) != 1. */
@tmpl succ_notone(x nat) { !eq(succ(x), 1) };

/* induction: The axiom of induction. */
@tmpl induction(P func(nat) bool) {
	P(1) && (x nat) { P(x) ==> P(succ(x)) }
==> (x nat) { P(x) }
};

/* application: This is a bit of a red-herring, present because i2's logical
 * kernel currently has a very superficial understanding of quantification. */
@tmpl application(P func(nat) bool, w nat) {
	(x nat) { P(x) } ==> P(w)
};

And now for the proof, which is of the theorem that for all natural numbers xxx
we have succ(x)≠x. succ(x) \ne x. succ(x)=x.

tmpl thm2(x nat) { !eq(succ(x), x) } {
base:	this(1)
<== { succ_notone(1) }
	true;

induct: (x nat) {
		this(x)
	==> { thm1(succ(x), x) }
		this(succ(x))
	};

	base && induct
==> { induction(this) }
	(x nat) { this(x) }
==> { application(this, x) }	
	this(x);
};

There are many mouthfuls in these two examples, and indeed, many things that
need to change, some that we can see (like the issue with quantification) and
some that we cannot (but you may).


GETTING STARTED

There are two ways of working with i2. If you are comfortable working from the
command line:

git clone https://git.sr.ht/~lbnz/i2
cd i2 && make
./bin/i2 examples/landau/addition-induction.i2


CREDIT

The theme here is based on the Hare programming language's site.