Kata

Task

Find out the proper definition of some basic logic constants and connectives in Rust under the well-known propositions-as-types paradigm, mainly complete the definition of these connectives and implement their constructor & deconstructor in given trait. Then prove some tautology about these connectives by constructing values which have the corresponding types

It can be hacky, since the type system of Rust is affine, you may need to utilize Clone + 'static and do some workaround. Note that although there are many different abnormal approaches (such as panic! or loop) to obtain a value of any type in Rust, this quiz will check the expected computational behaviours of these propositions to ensure their correctness. Moreover, the unsafe feature is forbidden in Prelude.

Preliminaries

The only indispensable skill to complete this kata is programming in Rust. However, some experience in logical reasoning can be helpful to play with this kata. For those who already known what Curry-Howard correspondence is, this kata can be a quiz about Rust programming language.

Propositions as Types, Proofs as Programs

It turns out that there are certain similarities in computer programming and logical reasoning, mainly the propositions as types, proofs as programs paradigm. In this paradigm, we can regard logical propositions as the type of programs, and the proof of propositions as programs. Thus it is possible to utilize programming languages as a proof assistant: to check if a program (value) is well-typed is exactly the same with to verify if it is a proof of certain proposition.

In this quiz we are focused on the minimal propositional logic, i.e., the truth constant and the conjunction, disjunction and implication connectives.

Top

Top is the truth constant, it holds unconditionally. Its proof should always be available.

trait Unit: Clone {
    fn inhabit() -> Self;
}

impl Unit for Top { fn inhabit() -> Self { unimplemented!() } 

Conj

Conj is the conjunction connective, it holds if all of its subpropositions hold. Its proof can be constructed when we supply proofs of all of its subpropositions, and we are able to extract these components when we needed.

trait Prod<A: Clone, B: Clone>: Clone {
    fn fst(self) -> A;
    fn snd(self) -> B;
    fn cons(fst: A, snd: B) -> Self;
}

impl<A: Clone, B: Clone> Prod<A, B> for Conj<A, B> {
    fn fst(self) -> A { unimplemented!() }
    fn snd(self) -> B { unimplemented!() }
    fn cons(fst: A, snd: B) -> Self { unimplemented!() }
}

Disj

Disj is the disjunction connective, it holds if one of its subpropositions holds. Its proof can be constructed when we supply a proof of any of its subpropositions, and we can do case analysis on such a proof to consume it.

trait Sum<A: Clone, B: Clone>: Clone {
    fn inl(left: A) -> Self;
    fn inr(right: B) -> Self;
    fn patmat<C>(self, left: impl Arrow<A, C>, right: impl Arrow<B, C>) -> C;
}

impl<A: Clone, B: Clone> Sum<A, B> for Disj<A, B> {
    fn inl(left: A) -> Self { unimplemented!() }
    fn inr(right: B) -> Self { unimplemented!() }
    fn patmat<C>(self, left: impl Arrow<A, C>, right: impl Arrow<B, C>) -> C {
        unimplemented!()
    }
}

Impl

Impl is the implication connective, it holds if whenever its antecedent holds, its succedent also holds. Its proof can be constructed when a proof of its succedent can be constructed depends on an arbitrary proof of its antecedent, and we are able to obtain a proof of the succedent of an implication by supplying a proof of its antecedent to convert it.

trait Arrow<A, B>: Clone {
    fn app(self, para: A) -> B;
    fn abs(fun: impl Fn(A) -> B + 'static) -> Self;
}

impl<A, B> Arrow<A, B> for Impl<A, B> {
    fn app(self, para: A) -> B { unimplemented!() }
    fn abs(fun: impl Fn(A) -> B + 'static) -> Self { unimplemented!() }
}

call/cc

call_cc_minimal is a relative negation (in minimal logic, A -> B can be regarded as the relative negation of A w.r.t. B) translation of the famous call-with-current-continuation operator, which can be typed by classical tautology ((A -> B) -> A) -> A (Peirce's law). It acts like the CPS translation version of call/cc, since various of CPS translation correspond to various of embeddings from minimal/intuitionistic logic into classical logic. Trying to implement an call/cc under given continuation may be easier than directly prove this proposition.

Supplementary Material: Witness of Truth

In the intuitionistic tradition, the validity of a statement is justified by some kind of term called its "proof", which witnesses its truth. These terms act like really proofs, i.e., one can effectively checking their construction to find out whether a proposition is valid, just like check a proof. If their construction procedures are inductively specified by a formal derivation with the conventional "proof" simultaneously, people may also call them "proof object".

The most famous proof objects are typed lambda calculi, which correspond to a wide range of logic (even classical), and they are also the simplest programming languages. Hence the structure of a term is ismorphic to a proof (since they are generated by same derivation), the simplification of such a term on one side corresponds to the normalization or cut-elimination of a proof. On the other side, the simplification also means executing this term (the program) and produce a value (the simplified term). This paradigm of establishing connections between various programming languages and logics via proof object is called the Curry-Howard correspondence.