From 3f6c0c153888229f3958c79af90610a48ac057b0 Mon Sep 17 00:00:00 2001
From: Ekaterina Goltsova <cache-nez@yandex.ru>
Date: Tue, 7 Jun 2022 17:02:18 +0200
Subject: [PATCH] Allow adding only constant (as opposed to schematic) symbols
to a running theory
This commit introduces the separation between Function/Predicate labels and
theory symbols. Both constant and schematic function labels behave as functions,
both constant and schematic predicate labels behave as predicates, but only
constant function and predicate labels can be symbols in a theory. This is now
expressed in the project by a marker trait TheorySymbol.
---
src/main/scala/lisa/kernel/Printer.scala | 2 +-
.../lisa/kernel/fol/CommonDefinitions.scala | 5 ++++
.../kernel/fol/FormulaLabelDefinitions.scala | 4 +--
.../kernel/fol/TermLabelDefinitions.scala | 2 +-
.../lisa/kernel/proof/RunningTheory.scala | 27 +++++++------------
.../lisa/settheory/SetTheoryDefinitions.scala | 18 ++++++-------
6 files changed, 28 insertions(+), 30 deletions(-)
diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index 3bac6470..044c181a 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -37,7 +37,7 @@ object Printer {
ConstantFunctionLabel("power_set", 1),
ConstantFunctionLabel("union", 1)
)
- private val nonAtomicPredicates = Set(equality, membership, subsetOf, sameCardinality) // Predicates which require parentheses (for readability)
+ private val nonAtomicPredicates: Set[PredicateLabel] = Set(equality, membership, subsetOf, sameCardinality) // Predicates which require parentheses (for readability)
private def prettyFormulaInternal(formula: Formula, isRightMost: Boolean, compact: Boolean): String = formula match {
case PredicateFormula(label, args) =>
diff --git a/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala b/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
index 3e34019f..65906e98 100644
--- a/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
@@ -20,6 +20,11 @@ private[fol] trait CommonDefinitions {
val id: String
}
+ /**
+ * Marks classes that can represent symbols in a theory
+ */
+ trait TheorySymbol
+
def freshId(taken: Set[String], base: String): String = {
var i = 0;
while (taken contains base + "_" + i) i += 1
diff --git a/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
index 81de8601..3439bc0a 100644
--- a/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -41,12 +41,12 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions {
/**
* A standard predicate symbol. Typical example are equality (=) and membership (∈)
*/
- final case class ConstantPredicateLabel(id: String, arity: Int) extends PredicateLabel
+ final case class ConstantPredicateLabel(id: String, arity: Int) extends PredicateLabel with TheorySymbol
/**
* The equality symbol (=) for first order logic.
*/
- val equality: PredicateLabel = ConstantPredicateLabel("=", 2)
+ val equality: ConstantPredicateLabel = ConstantPredicateLabel("=", 2)
/**
* A predicate symbol that can be instantiated with any formula.
diff --git a/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala b/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
index a7ca8288..24c501dc 100644
--- a/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
@@ -54,7 +54,7 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions {
* @param id The name of the function symbol.
* @param arity The arity of the function symbol. A function symbol of arity 0 is a constant
*/
- final case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel
+ final case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel with TheorySymbol
/**
* A schematic function symbol that can be substituted.
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index c68e8993..15175569 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -62,18 +62,12 @@ class RunningTheory {
private[proof] val theoryAxioms: mMap[String, Axiom] = mMap.empty
private[proof] val theorems: mMap[String, Theorem] = mMap.empty
- private[proof] val funDefinitions: mMap[FunctionLabel, Option[FunctionDefinition]] = mMap.empty
- private[proof] val predDefinitions: mMap[PredicateLabel, Option[PredicateDefinition]] = mMap(equality -> None)
+ private[proof] val definitions: mMap[TheorySymbol, Option[Definition]] = mMap(equality -> None)
/**
* Check if a label is a symbol of the theory
*/
- def isAcceptedFunctionLabel(label: FunctionLabel): Boolean = funDefinitions.contains(label)
-
- /**
- * Check if a label is a symbol of the theory
- */
- def isAcceptedPredicateLabel(label: PredicateLabel): Boolean = predDefinitions.contains(label)
+ def isSymbol(label: TheorySymbol): Boolean = definitions.contains(label)
/**
* From a given proof, if it is true in the Running theory, add that theorem to the theory and returns it.
@@ -108,10 +102,10 @@ class RunningTheory {
*/
def makePredicateDefinition(label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula): RunningTheoryJudgement[this.PredicateDefinition] = {
if (belongsToTheory(phi))
- if (!isAcceptedPredicateLabel(label))
+ if (!isSymbol(label))
if (phi.freeVariables.subsetOf(args.toSet) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
val newDef = PredicateDefinition(label, args, phi)
- predDefinitions.update(label, Some(newDef))
+ definitions.update(label, Some(newDef))
RunningTheoryJudgement.ValidJustification(newDef)
else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
else InvalidJustification("The specified symbol is already part of the theory and can't be redefined.", None)
@@ -141,7 +135,7 @@ class RunningTheory {
phi: Formula
): RunningTheoryJudgement[this.FunctionDefinition] = {
if (belongsToTheory(phi))
- if (!isAcceptedFunctionLabel(label))
+ if (!isSymbol(label))
if (phi.freeVariables.subsetOf(args.toSet + out) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j)))))
val r = SCProofChecker.checkSCProof(proof)
@@ -153,7 +147,7 @@ class RunningTheory {
val subst2 = bindAll(Forall, args.reverse, BinderFormula(ExistsOne, out, phi))
if (isSame(r.head, subst) || isSame(r.head, subst2)) {
val newDef = FunctionDefinition(label, args, out, phi)
- funDefinitions.update(label, Some(newDef))
+ definitions.update(label, Some(newDef))
RunningTheoryJudgement.ValidJustification(newDef)
} else InvalidJustification("The proof is correct but its conclusion does not correspond to a definition for for the formula phi.", None)
case _ => InvalidJustification("The conclusion of the proof must have an empty left hand side, and a single formula on the right hand side.", None)
@@ -201,7 +195,7 @@ class RunningTheory {
def belongsToTheory(phi: Formula): Boolean = phi match {
case PredicateFormula(label, args) =>
label match {
- case _: ConstantPredicateLabel => isAcceptedPredicateLabel(label) && args.forall(belongsToTheory)
+ case l: ConstantPredicateLabel => isSymbol(l) && args.forall(belongsToTheory)
case _: SchematicPredicateLabel => args.forall(belongsToTheory)
}
case ConnectorFormula(label, args) => args.forall(belongsToTheory)
@@ -222,7 +216,7 @@ class RunningTheory {
case VariableTerm(label) => true
case FunctionTerm(label, args) =>
label match {
- case _: ConstantFunctionLabel => isAcceptedFunctionLabel(label) && args.forall(belongsToTheory(_))
+ case l: ConstantFunctionLabel => isSymbol(l) && args.forall(belongsToTheory(_))
case _: SchematicFunctionLabel => args.forall(belongsToTheory(_))
}
@@ -261,14 +255,13 @@ class RunningTheory {
* For example, This function can add the empty set symbol to a theory, and then an axiom asserting
* the it is empty can be introduced as well.
*/
- def addSymbol(l: FunctionLabel): Unit = funDefinitions.update(l, None)
- def addSymbol(l: PredicateLabel): Unit = predDefinitions.update(l, None)
+ def addSymbol(s: TheorySymbol): Unit = definitions.update(s, None)
/**
* Public accessor to the set of symbol currently in the theory's language.
* @return the set of symbol currently in the theory's language.
*/
- def language: (List[(FunctionLabel, Option[FunctionDefinition])], List[(PredicateLabel, Option[PredicateDefinition])]) = (funDefinitions.toList, predDefinitions.toList)
+ def language: List[(TheorySymbol, Option[Definition])] = definitions.toList
/**
* Public accessor to the current set of axioms of the theory
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index 337e67fe..a2f3b2b7 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -16,20 +16,20 @@ private[settheory] trait SetTheoryDefinitions {
final val sPhi = SchematicPredicateLabel("P", 2)
final val sPsi = SchematicPredicateLabel("P", 3)
// Predicates
- final val in: PredicateLabel = ConstantPredicateLabel("set_membership", 2)
- final val subset: PredicateLabel = ConstantPredicateLabel("subset_of", 2)
- final val sim: PredicateLabel = ConstantPredicateLabel("same_cardinality", 2) // Equicardinality
+ final val in = ConstantPredicateLabel("set_membership", 2)
+ final val subset = ConstantPredicateLabel("subset_of", 2)
+ final val sim = ConstantPredicateLabel("same_cardinality", 2) // Equicardinality
final val predicates = Set(in, subset, sim)
// val application
// val pick
// Functions
- final val emptySet: FunctionLabel = ConstantFunctionLabel("empty_set", 0)
- final val pair: FunctionLabel = ConstantFunctionLabel("unordered_pair", 2)
- final val singleton: FunctionLabel = ConstantFunctionLabel("singleton", 1)
- final val powerSet: FunctionLabel = ConstantFunctionLabel("power_set", 1)
- final val union: FunctionLabel = ConstantFunctionLabel("union", 1)
- final val universe: FunctionLabel = ConstantFunctionLabel("universe", 1)
+ final val emptySet = ConstantFunctionLabel("empty_set", 0)
+ final val pair = ConstantFunctionLabel("unordered_pair", 2)
+ final val singleton = ConstantFunctionLabel("singleton", 1)
+ final val powerSet = ConstantFunctionLabel("power_set", 1)
+ final val union = ConstantFunctionLabel("union", 1)
+ final val universe = ConstantFunctionLabel("universe", 1)
final val functions = Set(emptySet, pair, singleton, powerSet, union, universe)
val runningSetTheory: RunningTheory = new RunningTheory()
--
GitLab