Disallow unbound type variables

[mezpusz]

The original intention of the PR was to fix #744, but I started with the assumption that we should disallow unbound type variables in all places. For example, we wouldn't allow an operator type of e.g. a function f to be !>[X0: $tType]:((map(X0,X1) * X0) > X1) but only !>[X0: $tType, X1: $tType]:((map(X0,X1) * X0) > X1) where all variables inside the type are prenex quantified.

I think this check would be reasonable to merge since unbound type variables of terms make the type variables fixed such that from then on those variables cannot be changed anywhere and X1 cannot be used for anything else in any formula/clause where f is present.

Then, to make this work I got to refactoring let binders which resulted in a big amounts of code refactored and removed. Not sure if all paths are covered, but this is a relatively stable iteration.

There may be also other theories/operators that needs "polymorphization" like arrays, but I will also leave those for the future.

[mezpusz]

I got the following "new" proof after some tuple related crash disappeared, but according to TPTP the problem is satisfiable. Maybe it would be good to look into this if we really merge the PR.

./vampire -newcnf on $TPTP/Problems/SYN/SYN000_4.p
% WARNING: debug build, do not use in anger
% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Unsatisfiable for SYN000_4
% SZS output start Proof for SYN000_4
8. ! [X0 : $int,X1 : $int] : max(X0,X1) = $ite($greatereq(X0,X1), (X0,X1) [input(axiom)]
9. ! [X0 : $int,X1 : $int] : $ite(max(X0,X1) = X0, ($greatereq(X0,X1),$greatereq(X1,X0)) [input(axiom)]
11. ! [X0 : $int,X1 : $int] : dct1 = $ite($greater(X0,X1), (tuple4($int,$int,X0,X1),tuple4($int,$int,X1,X0)) [input(axiom)]
21. ! [X0 : $int,X1 : $int] : max(X0,X1) = $ite(~$less(X0,X1), (X0,X1) [theory normalization 8]
22. ! [X0 : $int,X1 : $int] : $ite(max(X0,X1) = X0, (~$less(X0,X1),~$less(X1,X0)) [theory normalization 9]
24. ! [X0 : $int,X1 : $int] : dct1 = $ite($less(X1,X0), (tuple4($int,$int,X0,X1),tuple4($int,$int,X1,X0)) [theory normalization 11]
29. $sum(X0,X1) = $sum(X1,X0) [tha commutativity]
30. $sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2) [tha associativity]
33. 0 = $sum(X0,$uminus(X0)) [tha inverse op unit]
34. ~$less(X0,X0) [tha non-reflexivity]
38. $less(X1,$sum(X0,1)) | $less(X0,X1) [tha order plus one dichotomy]
40. ~$less(X1,$sum(X0,1)) | ~$less(X0,X1) [tha extra integer ordering]
47. tuple4(X0,X1,X4,X6) != tuple4(X0,X1,X5,X7) | X6 = X7 [term algebras injectivity axiom]
51. ! [X0 : $int,X1 : $int] : $ite(max(X0,X1) = X0, (~$less(X0,X1),~$less(X1,X0)) [rectify 22]
68. $less(X0,X1) | max(X0,X1) = X0 [cnf transformation 21]
71. max(X0,X1) != X0 | ~$less(X0,X1) [cnf transformation 51]
73. $less(X1,X0) | tuple4($int,$int,X1,X0) = dct1 [cnf transformation 24]
105. $less(X0,$sum(X0,1)) [resolution 38,34]
111. $less(X0,$sum(1,X0)) [superposition 105,29]
120. ~$less(X1,X0) | max(X0,$sum(X1,1)) = X0 [resolution 68,40]
194. $sum(0,X1) = $sum(X0,$sum($uminus(X0),X1)) [superposition 30,33]
215. $sum(X0,$sum($uminus(X0),X1)) = X1 [evaluation 194]
243. dct1 = tuple4($int,$int,X0,X0) [resolution 73,34]
361. $less($sum($uminus(1),X0),X0) [superposition 111,215]
364. $less($sum(-1,X0),X0) [evaluation 361]
433. $less($sum(X0,-1),X0) [superposition 364,29]
487. dct1 != tuple4($int,$int,X1,X2) | X0 = X2 [superposition 47,243]
497. max(X0,$sum(X1,1)) = X0 | tuple4($int,$int,X1,X0) = dct1 [resolution 120,73]
523. max(X0,$sum(X1,1)) = X0 [forward subsumption resolution 497,487]
527. X0 != X0 | ~$less(X0,$sum(X1,1)) [superposition 71,523]
528. ~$less(X0,$sum(X1,1)) [trivial inequality removal 527]
546. $false [resolution 528,433]
% SZS output end Proof for SYN000_4
Condition in file /Users/mezpusz/vampire/Shell/UIHelper.cpp, line 496 violated:
!s_expecting_sat
----- stack dump -----
Version : Vampire 5.0.0 (Debug build, commit b18e52409 on 2025-11-20 17:04:19 +0100)
(use '--traceback on' to invoke a debugger and get a human-readable stack trace)
----- end of stack dump -----

[quickbeam123]

Having a quick look at ./vampire -newcnf on $TPTP/Problems/SYN/SYN000_4.p

1. the $ite( printing does not seem to be providing the closing )
2. I would say Geoff is wrong about the status. The following is the suspicious bit:

tff(ite_4,axiom,
    ! [X: $int,Y: $int] :
      ( dct1 = $ite($greater(X,Y),[X,Y],[Y,X]) ) ).

It's a bit hidden behind the tuple mess, but dct1 is declared as a constant, but intended was probably a function of arity 2 (of X and Y) as the axiom insists dct1 has many values!

[mezpusz]

1. the $ite( printing does not seem to be providing the closing )

Yes, special terms have an extra opening parenthesis because otherwise the initial special arguments wouldn't be separated from the functor by any parenthesis. This (and other problems, for example with tuples) could be solved e.g. by separating the logic for parentheses (or brackets, etc.), similarly as we separate outputting the header with headerToString().

[mezpusz]

2. I would say Geoff is wrong about the status. The following is the suspicious bit:

I think the proof looks relatively straightforward, so I wouldn't worry about unsoundness here either. I can write Geoff an email.

[MichaelRawson]

This is really nice, we get rid of some evil SpecialTerms and fix the $let-binding properly. I trust you got all the miscellaneous changes in the rest of Vampire right, and the core changes look good to me.

[mezpusz]

CI build: Error: The operation was canceled.

Phew, I thought I messed something up.

[MichaelRawson]

Yeah, sorry - I wish it gave more informative e-mail when it's cancelled rather than failed. Gotta save those cycles.