FO Sequent: Error when using allLeft or exRight

[Drodt]

When using allLeft or exRight in the FO sequent calculus and instantiating with a term that is not a simple constant, e.g., f(a), the following error is shown by the UI:

Character at position 1 in 'f(a)' is not allowed in constants

How to reproduce:

1. Enter \all X: P(X) -> P(f(a))
2. Use impRight
3. Use allLeft with f(a)
4. Get the error

[rec0de]

Follow up question while I'm looking at the code:

There's an unimplemented function findFittingVariableName that would implement some sort of proof-search for fitting instantiations in allLeft and exRight if no instantiation is given. Currently this just throws an exception.

However, the same function is used in allRight and exLeft to get what should be a fresh constant (?) if none is given explicitly. This is incorrect, no? If anything, there should be a second getFreshVariable function.

https://github.com/KalkulierbaR/kalkulierbar/blob/0792fb921eace281b8f77f146a3d82d32ff32db3/backend/src/main/kotlin/kalkulierbar/sequent/fosc/BasicMoves.kt#LL146C39-L146C39

[Drodt]

Yes, much of the logic there is incorrect. I am currently working on a fix (the backend is fixed) but I am stuck at the frontend. Basically, I had to update some dependencies to newer versions, which are now incompatible with the other dependencies, etc. That will take some time to fix.

I will look into implementing findFittingVariableName which shouldn't be too hard.

I also want to collect all signatures of functions in the formula. It should not be allowed to write, e.g., f(a, b) if f was a unary function before. We check this during parsing, right?

[rec0de]

We don't. I think f(a, b) and f(a) would be treated as different functions for most purposes? There's some potential for weirdness there because identifier freshness-checks ignore arity. So if you have a function f(a) you won't be able to instantiate a fresh constant f.

Should be pretty straightforward though to write a collector that gathers all functions and their signatures / arities so you can check for conflicting instantiations (and initial consistency on the initial parse).

Also feel free to push the backend fixes before the frontend is ready :)

See

kalkulierbar/backend/src/main/kotlin/kalkulierbar/logic/transform/Collectors.kt

Lines 78 to 137 in 0792fb9

	class IdentifierCollector : DoNothingCollector() {
	companion object {
	private val instance = IdentifierCollector()
	/**
	* Collect a set of all identifiers used in a formula
	* Including: Variables, constants, function- and relation names
	* @param formula Formula to collect identifiers from
	* @return Set of all identifiers found
	*/
	fun collect(formula: LogicNode): Set<String> {
	instance.identifiers.clear()
	formula.accept(instance)
	return instance.identifiers
	}
	}
	private val identifiers = mutableSetOf<String>()
	private val termIdCollector = TermIdentifierCollector(identifiers)
	override fun visit(node: Relation) {
	identifiers.add(node.spelling)
	node.arguments.forEach {
	it.accept(termIdCollector)
	}
	}
	override fun visit(node: UniversalQuantifier) {
	identifiers.add(node.varName)
	node.child.accept(this)
	}
	override fun visit(node: ExistentialQuantifier) {
	identifiers.add(node.varName)
	node.child.accept(this)
	}
	}
	/**
	* Collects identifiers (function names, constants, variable names)
	* from first order terms
	* @param identifiers Set of identifiers to add found identifiers to
	*/
	class TermIdentifierCollector(private val identifiers: MutableSet<String>) : FirstOrderTermVisitor<Unit>() {
	override fun visit(node: Constant) {
	identifiers.add(node.spelling)
	}
	override fun visit(node: QuantifiedVariable) {
	identifiers.add(node.spelling)
	}
	override fun visit(node: Function) {
	identifiers.add(node.spelling)
	node.arguments.forEach {
	it.accept(this)
	}
	}
	}

[rec0de]

Also, if you're already touching the frontend, I think adding an 'automatic' button to the fresh constant assignments in exLeft and allRight (which just sends a null assignment) would be a super cheap quality of life improvement (with an implementation of a freshConstant function in the backend but that's also cheap)

[Drodt]

allLeft and exRight

Do you mean allRight and exLeft or am I misunderstanding?

[Drodt]

Also, see #105

[rec0de]

Do you mean allRight and exLeft or am I misunderstanding?

Yes, sorry - copy pasted from the wrong reply.

[Drodt]

Great, then I'll add it to my TODO