- Notifications
You must be signed in to change notification settings - Fork0
A reasonable theorem prover for your reasoning tasks!
License
adam-mcdaniel/reckon
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
Reckon is a programming language designed for reasoning tasks, proof checking, and logical inferencing. Its syntax is a variant of Prolog, so it's easy to learn and use if you're already familiar with logic programming or propositional logic.
The language is still in its early stages of development, so there are many features that are not yet implemented. However, the core functionality is there, and you can already write and run simple programs in Reckon.
To get started with Reckon, you'll need to have the following installed on your machine:
Once you have Rust and Cargo installed, you can clone this repository and install the interpreter with Cargo:
$cd~/Downloads$ git clone https:%github.com/adam-mcdaniel/reckon.git$cd reckon$ cargo install --path.
Now you should be able to run the Reckon interpreter from the command line:
$ reckon
This will start the Reckon REPL, where you can begin to enter your rules and queries!
For more information on how to use the REPL commands, type:help in the REPL.
Although Reckon is a CLI tool, I mainly designed it to be used as a library to perform reasoning tasks within code.
To use Reckon as a library, add the following to yourCargo.toml file:
[dependencies]reckon = {git ="https://github.com/adam-mcdaniel/reckon" }
Then, you can use Reckon in your Rust code like the example below.If you know how to write Reckon code, it's very easy to integrate it into your Rust code.
The following example demonstrates how we can use theprove_true function to find a single solution to a query using the Reckon library.
use reckon::*;fnmain(){// Define some rules to use for inferencelet rules:Vec<Rule> =vec!["is_nat(s(X)) :- is_nat(X).".parse().unwrap(),"is_nat(0).".parse().unwrap(),"add(X, s(Y), s(Z)) :- add(X, Y, Z).".parse().unwrap(),"add(X, 0, X) :- is_nat(X).".parse().unwrap(),];// Create a new environment with the rulesletmut env =Env::<DefaultSolver>::new(&rules);// Define a query to find two numbers that add to 4let query:Query ="?- add(A, B, s(s(s(s(0))))).".parse().unwrap();// You can use the `prove_true` method to find a single solution,// or the `prove_false` method to check if the query is false.match env.prove_true(&query){Ok(solution) =>{println!("Found proof: ");println!("{}", solution);}Err(e) =>eprintln!("Unproven terms: {:?}", e)}}
This code will output the following:
Found proof: Solutionfor query:?- add(A, B, s(s(s(s(0))))).Final query:?-.Variable bindings:A = 0B = s(s(s(s(0))))
We can also use thefind_solutions function to find multiple solutions to a query.This allows us to exhaustively search for all possible solutions to a query,until the depth fails or the solution limit is reached. You can optionally set a step limit in the search configuration, if you want to guarantee an answer within a certain amount of time.
use reckon::*;fnmain(){// Define some rules to use for inferencelet rules:Vec<Rule> =vec!["is_nat(s(X)) :- is_nat(X).".parse().unwrap(),"is_nat(0).".parse().unwrap(),"add(X, s(Y), s(Z)) :- add(X, Y, Z).".parse().unwrap(),"add(X, 0, X) :- is_nat(X).".parse().unwrap(),];// Create a new environment with the rulesletmut env =Env::<DefaultSolver>::new(&rules)// Set the solution limit to 4 for the following queries.with_search_config(SearchConfig::default().with_solution_limit(4));// Define a query to find two numbers that add to 4let query:Query ="?- add(A, B, s(s(s(s(0))))).".parse().unwrap();// Alternatively, find multiple solutions to the querymatch env.find_solutions(&query){Ok(solutions) =>{// For each solution found, print the variable bindingsfor(i, solution)in solutions.iter().enumerate(){println!("Solution #{}: ", i +1);for(var, binding)in solution{println!("{} = {}", var, binding);}}}// Unsolved goalsErr(e) =>eprintln!("Unproven terms: {:?}", e)}}
This code will output the following:
Solution#1:A = 0B = s(s(s(s(0))))Solution#2:A = s(s(0))B = s(s(0))Solution#3:A = s(s(s(0)))B = s(0)Solution#4:A = s(0)B = s(s(s(0)))
Theexamples directory contains a few example programs that you can run inthe Reckon interpreter.
The subsection below shows some of these examples.
Here's an example Reckon program that does some more complex arithmetic:
% Define the natural numbersis_nat(s(X)):- is_nat(X).is_nat(0).% Define addition of natural numbersadd(X,0,X):- is_nat(X).add(X, s(Y), s(Z)):- add(X,Y,Z).% Define multiplication of natural numbersmul(X, s(Y),Z):- mul(X,Y,W), add(X,W,Z).mul(X,0,0):- is_nat(X).% Define less-than-or-equal-to relation on natural numbersleq(0,X):- is_nat(X).leq(s(X), s(Y)):- leq(X,Y).% Define greater-than-or-equal-to relation on natural numbersgeq(X,Y):- leq(Y,X).% Define equality relation on natural numberseq(X,Y):- leq(X,Y), leq(Y,X).neq(X,Y):- ~eq(X,Y).% Define less-than relation on natural numberslt(X,Y):- leq(X,Y), ~eq(X,Y).% Define greater-than relation on natural numbersgt(X,Y):- geq(X,Y), ~eq(X,Y).% Define the square relation, Y is the square of X if Y = X^2square(X,Y):- mul(X,X,Y).% Find two numbers whose sum is 4?- add(A, B, s(s(s(s(0))))).% Find three numbers A, B, C such that A + B = C and A <= 3, B <= 3, C <= 4, and A + A != 4?- ~add(A, A, s(s(s(s(0))))), add(A, B, C), leq(A, s(s(s(0)))), leq(B, s(s(s(0)))), leq(C, s(s(s(s(0))))).% Set the solution limit to 1 for the following queriesoptions(solution_limit=1).% Find a natural number X such that X^2 = 2 (no solution)?- square(X, s(s(0))).% false
To run this example (arithmetic.rk), use thereckon command line program with the file as an argument:
$ reckon examples/arithmetic.rk
This yields the following output:
Below is an example Reckon program that implements some rules forSystem F.
System F is a typed lambda calculus that extends the simply typed lambda calculus with universal quantification. It is a powerful language for reasoning about polymorphic functions and types. It's used in many functional programming languages, such as Haskell.
It's also pretty complex, so this example is a bit more involved than the previous one.
options(depth_limit=500,width_limit=5,traversal="breadth_first",pruning=false,require_rule_head_match=true,reduce_query=false,solution_limit=1,clean_memoization=true).term(var(X)):- atom(X).atom(X).% Lambda abstractionterm(abs(X,T,Body)):- atom(X), type(T), term(Body).% Applicationterm(app(Func,Arg)):- term(Func), term(Arg).% Type abstraction (universal quantification: ΛX. T)term(tabs(TVar,Body)):- atom(TVar), term(Body).% Type application (specializing a polymorphic type: T [τ])term(tapp(Func,T)):- term(Func), type(T).% Base typestype(base(T)):- atom(T).% Example: `int`, `bool`% Arrow types (functions)type(arrow(T1,T2)):- type(T1), type(T2).% Example: T1 -> T2% Universal quantifiers (∀X. T)type(forall(TVar,T)):- atom(TVar), type(T).bind(X,T):- atom(X), type(T).context(nil).context([]).context([bind(X,T) |Rest]):- atom(X), type(T), context(Rest).member(X, [X |_]).member(X, [_ |Rest]):- member(X,Rest).has_type(Ctx, var(X),T):- member(bind(X,T),Ctx).has_type(Ctx, abs(X,T,Body), arrow(T,TBody)):- has_type([bind(X,T) |Ctx],Body,TBody).has_type(Ctx, app(Func,Arg),T2):- has_type(Ctx,Func, arrow(T1,T2)), has_type(Ctx,Arg,T1).has_type(Ctx, tabs(TVar,Body), forall(TVar,TBody)):- has_type(Ctx,Body,TBody).has_type(Ctx, tapp(Func,Type),TSubstituted):- has_type(Ctx,Func, forall(TVar,TBody)), substitute(TBody,TVar,Type,TSubstituted).eq(T1,T1).eq(base(T1), base(T2)):- eq(T1,T2).eq(arrow(T1,T2), arrow(T3,T4)):- eq(T1,T3), eq(T2,T4).eq(forall(X,T1), forall(X,T2)):- eq(T1,T2).% Bodies of the quantified types must be equalneq(T1,T2):- ~eq(T1,T2).% Substitution base case: If the type is the type variable being substituted, replace it.substitute(base(T),TVar,Replacement,Replacement):- eq(T,TVar).% If the type is not the variable being replaced, leave it unchanged.substitute(base(T),TVar,_, base(T)):- eq(T,TVar).% For arrow types, substitute in both the domain and codomain.substitute(arrow(T1,T2),TVar,Replacement, arrow(T1Sub,T2Sub)):- substitute(T1,TVar,Replacement,T1Sub), substitute(T2,TVar,Replacement,T2Sub).% For universal quantifiers, substitute in the body only if the bound variable is not the same.substitute(forall(TVarInner,TBody),TVar,Replacement, forall(TVarInner,TBodySub)):- neq(TVar,TVarInner),% Avoid variable capture substitute(TBody,TVar,Replacement,TBodySub).?- has_type([], abs(x, base(int), abs(y, base(float), var(x))), T).
The query at the end of the program, which is repeated below, asks whether the termabs(x, base(int), abs(y, base(float), var(x))) has a typeT in the empty context.
The termabs(x, base(int), abs(y, base(float), var(x))) is a lambda abstraction that takes an integerx and a floaty and returnsx. The expected type of this term isint -> float -> int.
The only way the program can deduce the typeint -> float -> int for this term is if it can infer that the body of the innermost lambda abstraction has typeint. It must do this by adding the type ofx to the context, and then retrieving it when checking the type ofvar(x) in the body of the innermost lambda.
?- has_type([], abs(x, base(int), abs(y, base(float), var(x))), T).
As expected, the program successfully deduces that the termabs(x, base(int), abs(y, base(float), var(x))) has typeint -> float -> int:
The documentation for this project is hosted onGitHub Pages, athttps://adam-mcdaniel.github.io/reckon.
This documentation is generated usingRustdoc andmdBook.
To generate the documentation locally, run the following commands:
$ cargo doc --no-deps
This will generate the documentation in thetarget/doc directory.
If you haveDune shell installed, you can use thebuild-docs.dunesh script to generate thedocs folder for the GitHub Pages site.This will allow the documentation to show the images correctly.
$ use ./build-docs.dunesh
This project is licensed under the MIT License. See theLICENSE file for details.
Hello,I'm Adam McDaniel, a software engineer and computer science PhD student at the University of Tennessee Knoxville. I'm passionate about programming languages, compilers, and formal methods. I'm a huge fan of Rust and functional programming, and I love building tools that help people write better software.
Here's some interesting links for some of my other projects:
| Website |
|---|
| My programming language🧑💻 |
| My shell🐚 |
| My blog📝 |
| My YouTube📽️ (compilers and music) |
About
A reasonable theorem prover for your reasoning tasks!