oxilean_std/program_extraction/
types.rs

1//! Types for program extraction from constructive proofs (Curry-Howard correspondence).
2
3/// A constructive proposition in intuitionistic logic.
4#[derive(Debug, Clone, PartialEq, Eq)]
5pub enum ConstructiveProp {
6    /// Logical truth (⊤).
7    True,
8    /// Logical falsehood (⊥).
9    False,
10    /// Conjunction (P ∧ Q).
11    And(Box<ConstructiveProp>, Box<ConstructiveProp>),
12    /// Disjunction (P ∨ Q).
13    Or(Box<ConstructiveProp>, Box<ConstructiveProp>),
14    /// Negation (¬P), defined as P → ⊥.
15    Not(Box<ConstructiveProp>),
16    /// Implication (P → Q).
17    Implies(Box<ConstructiveProp>, Box<ConstructiveProp>),
18    /// Existential quantification (∃x. P(x)).
19    Exists(String, Box<ConstructiveProp>),
20    /// Universal quantification (∀x. P(x)).
21    Forall(String, Box<ConstructiveProp>),
22    /// Atomic proposition with arguments.
23    Atom(String, Vec<String>),
24    /// Propositional equality of two terms.
25    Eq(String, String),
26}
27
28/// A proof term in the Curry-Howard correspondence.
29/// Each term witnesses a constructive proof of some proposition.
30#[derive(Debug, Clone, PartialEq, Eq)]
31pub enum ProofTerm {
32    /// Witness for ⊤ (unit).
33    Unit,
34    /// Witness for P ∧ Q (pair of proofs).
35    Pair(Box<ProofTerm>, Box<ProofTerm>),
36    /// First projection of a pair (proof of P from proof of P ∧ Q).
37    Fst(Box<ProofTerm>),
38    /// Second projection of a pair (proof of Q from proof of P ∧ Q).
39    Snd(Box<ProofTerm>),
40    /// Left injection into a disjunction (proof of P ∨ Q from proof of P).
41    Inl(Box<ProofTerm>),
42    /// Right injection into a disjunction (proof of P ∨ Q from proof of Q).
43    Inr(Box<ProofTerm>),
44    /// Lambda abstraction (proof of P → Q).
45    Lambda(String, Box<ProofTerm>),
46    /// Function application (modus ponens).
47    App(Box<ProofTerm>, Box<ProofTerm>),
48    /// Existential witness packing (pack a witness with a proof).
49    Pack(String, Box<ProofTerm>),
50    /// Existential witness unpacking.
51    Unpack {
52        /// The variable binding the witness value.
53        witness: String,
54        /// The variable binding the proof of the body proposition.
55        proof_var: String,
56        /// The term being unpacked.
57        packed: Box<ProofTerm>,
58        /// The body using the unpacked witness and proof.
59        body: Box<ProofTerm>,
60    },
61    /// Proof by contradiction / ex falso quodlibet from ⊥.
62    Absurd(Box<ProofTerm>),
63    /// Variable reference.
64    Var(String),
65}
66
67/// A program extracted from a constructive proof via Curry-Howard.
68#[derive(Debug, Clone, PartialEq, Eq)]
69pub struct ExtractedProgram {
70    /// Name of the extracted program.
71    pub name: String,
72    /// Type of the input (as a string description).
73    pub input_type: String,
74    /// Type of the output (as a string description).
75    pub output_type: String,
76    /// The extracted program body as a proof term.
77    pub body: ProofTerm,
78    /// The original constructive proposition this program proves.
79    pub original_prop: ConstructiveProp,
80}
81
82/// A Hoare-style specification for a program.
83#[derive(Debug, Clone, PartialEq, Eq)]
84pub struct ProgramSpec {
85    /// Precondition (must hold before execution).
86    pub pre: ConstructiveProp,
87    /// Postcondition (must hold after execution).
88    pub post: ConstructiveProp,
89    /// Name of the specified program.
90    pub name: String,
91}
92
93/// Result of a program extraction attempt.
94#[derive(Debug, Clone, PartialEq, Eq)]
95pub enum ExtractionResult {
96    /// Successful extraction yielding a program.
97    Success(ExtractedProgram),
98    /// The proposition is not constructive (contains classical reasoning).
99    NonConstructive(String),
100    /// Extraction failed for some other reason.
101    Failure(String),
102}
oxilean_std/program_extraction/types.rs

oxilean_std/program_extraction/
types.rs
