r''' \documentclass{article} \title{Literate programming version of the graph stratification algorithm version of the Marcel prover} \author{Lavinia Randall Holmes} \usepackage{verbatim} \usepackage{amssymb} \usepackage{bussproofs} \usepackage{amssymb} \usepackage{latexsym} \begin{document} \maketitle \tableofcontents \subsection{version remarks} Graph stratification version of the Marcel theorem prover, 6/7/2026 by (Lavinia) Randall Holmes, intellectual property rights to be respected to the extent of preserving this attribution, please. \begin{description} \item[6/7/2026:] savethproof and loadproof commands now are recorded to logs \item[6/6/2026:] The {\tt savetheproof} and {\tt loadproof} arguments have been installed, allowing one to leave a proof, prove a required lemma, then rejoin it at the same point. \item[6/2/2026:] Installed digits as definienda. Fixed harmless bug which posted definienda to the variable list. Installed a brief construction for entering arguments to let terms. \item[5/31/2026:] Notes to self as I edit. The occurrence index counter might need to be updated when {\tt theoremcut} is executed. This might be faked using a substitution. Addressed this issue: the cut instance of the theorem has all new occurrence indices. It is worth noting (because this concerned me) that there is no such problem for definitions: defexpand already updates occurrences. It remains interesting to try to improve the display of stratifications, though the ones actually displayed in normal work, the cycles witnessing stratification failure and the type tables for definitions, are actually pretty readable at this point. \item[5/29/2026:] The self-documented literate programming version of this code. \item[5/28/2026:] The literate programming version. Getting rid of most earlier update comments. \item[5/27/2026:] Quite a lot has been added today. 1. Made the variable space used for let terms (definitions) completely disjoint from variables which can be entered or displayed. This makes evaluation of definitions secure from variable capture problems. 2. Fixed soundness problems with dynamic setting of unknowns. An unknown is to be matched only once, and its match is recorded (for the equality function to make checks for consistency). Also, realized that higher order matching had no unknown dependency checks. 3. Further, equality tests will now attempt to establish equality by definition expansion. This may have various fancy effects. It is a fun point that though I did a lot of work today it appears to have no effect on existing scripts. \item[5/27/2026:] The equality functions now test whether definition expansion will make terms equal. The unknown setting feature is unsound and needs to be repaired. installed a fix: dare I test it? Fix seems to work... It is very important that done() appears to be the only client of the equality tests. Any client needs to appropriately reset unknownassignments. Also added unknown dependency checks to the higher order matching. There needs to be a lot of tightening. \item[5/27/2026:] More variable security needed for the definition facility. the @ variables used in substitutions into definitions cannot be allowed to be generated in user entered or even generated text. The appearance is exactly the same as before, but function names in the code may be annoying due to the history of my thought process while correcting this problem : the hash is now the variable prefix used internally (so atify functions add hashes) and the at sign @ is used externally as before (so hashify adds @ and deatify changes to @) But the variables used for definition (let term) computation are now completely secure: no user operation can produce them, so no variable capture can occur in let term computation. theoremcut now atifies ("hashifies") the new formula introduced, so that free variables in theorems will not intrude in the usual namespace. they can be manipulated using setunknown to be replaced with terms containing no fresh variables, which gives them very limited privileges. Free variables left over from definitions will be treated similarly. I still havent fixed apparent variable capture ;-) It is philosophically appealing but probably not practical that I somehow do not have to. \end{description} \section{Introduction} This is an alternative development of the core of the Marcel sequent prover for stratified set theory. The immediate occasion for starting this project was consideration of Ryan Nolan's use of the Bellman-Ford algorithm to test stratification: using Bellman-Ford is a bad idea, because the second time that you relax or even have the opportunity to extend an edge [something that Bellman-Ford won't even notice] you should abort and report stratification failure. Here I describe a more sensible graph based algorithm for stratification testing, which can be thought of as a variant of Dijsktra's algorithm. This is also informed by the fact that Forster and I are working right now, quite independently, on the properties of the graph determined by the atomic formulas in a formula: we are particularly interested in connectedness of this graph, and the stratification testing in this version is very weak, even weaker than Marcel's weak stratification: all that is required is that occurrences of variables connected to the binding variable in a set abstract be typed sensibly relative to that variable. Variables in terms and formulas of the language used here have occurrence data attached to them invisibly [and it is occurrences that have relative type, not variables per se], which has odd effects, not only enabling weak stratification, but also removing the effects of bound variable capture (though I really should modify the display function to warn the viewer about apparent bound variable capture: the system can tell when some variables in the scope of a bound variable are actually free with the same shape, but it does not warn the viewer when this happens; the system does prevent the binding of the free ``fresh variables" introduced by the quantifier rules. It is important to note that the basic stratification condition, that the lengths of all paths between the same pair of variables are the same, was stated (in an incorrect form) by Quine in the original NF paper, and the correction allowing paths to contain converse membership (with negative length) as well as membership with positive length (and equality with zero length) was proposed (as a correction to Quine) by Thomas Forster years ago. Nolan was an incidental inspiration to the present effort, but had not proposed anything not prefigured in earlier work: and what we do is actually quite different. It is a nod to Nolan that the data reported on stratification failure is a cycle of nonzero length in the graph associated with a formula. This version has NF extensionality, but could easily be converted to SF or NFU. I do think there are interesting advantages to working with a fully extensional theory. Other things to notice is that this version has Polish notation input (so far): this is handy for quick prototyping. The output notation is somewhat more familiar. The sequent prover is quite similar to previous versions, but if anything more streamlined. Marcel enjoys a very limited set of commands, as the execution of most sequent rules is simply ``apply the appropriate rule to the left or right sequent''. Using a list with reference pointers gives a much more sensible proof structure than the tree structure I used in previous versions. The very efficient and liberal stratification algorithm is nice, though I think the method I used last time of requiring type indices on bound variables worked quite well as well. The way I handled defined notions is new with this version. It is motivated in some details by the needs of the graph stratification algorithm. It allows introduction of defined notions with any arity and allows arguments to be supplied in any order (though I haven't exploited this). The support for infix display is amusing. The automatic matching of unknown variables is expanded to higher order in this version. The idea is to avoid having to use {\tt setunknown} too often. The fact that my scripts are actually Python programs may be useful, and the addition of display information to them makes them more intelligible and perhaps easier to debug, though larger. Things which could be added: \begin{itemize} \item Decluttering of sequents (pruning propositions from left or right) should be supported. The autopruning feature of previous versions of Marcel makes for more economical saved formal proofs. \item It would be nice to have a parser for something more like the output notation. An approach might be to parse with the Polish notation as the target, then check by applying the display function that we got the right thing. \item Automatic generation of cut free proofs (normalization) would be interesting. \item I have never made any particular attempt to write tactics for Marcel in any of its versions. Perhaps I should think about this. \item I should work on an interactive script editor to make it easier to correct a script (if the proof strategy needs to be changed, or if a change in the code messes up its behavior). One envisions the ability to run a script in demo mode, but also to be able to drop in and change a command and/or insert or delete some commands, and then resume. A related idea would be construction of proofs from scripts, or designing scripts to be as far as possible stable after code changes. \item Can the definition facility be modified to enable safe use of definitions of unstratified concepts? \item Do we want additional primitives, such as pairs and projections, relation and function abstraction, and so forth? What about defined binding constructions? \end{itemize} \subsection{Philosophical considerations} The author is tempted to contemplate Marcel as an implementation of the program of the original New Foundations paper. We maintain, in line with what Quine actually says, is that the purpose of the paper was not to propose a weird new set theory, though that was its practical effect. The purpose of the paper was to explore the logicist viewpoint of the foundations of mathematics. Quine was at pains to minimize his primitives (probably to be sure that they were logical). He uses the Sheffer stroke and the universal quantifier to cover the ground of first order logic. We adopt more primitives, but of course they are all definable in terms of Quine's primitives, and Quine defines all of them and makes essential use of them. It might be fun in this connection to add the Sheffer stroke with suitable sequent rules to our machinery, to support the demonstration of its sufficiency. Our style of first order logic proof is different from Quine's. But the state of the art has improved. The final primitive is membership. In this connection we have two concerns to air. The first is whether membership is a logical notion. What we say on this is, {\em predication\/} is certainly a logical notion, and membership is a case of predication. The additional element is that we are given a criterion (stratification) for allowing reification of a predicate. Reification of predicates is needed because in $x \in y$, $y$ represents a predicate to be considering as holding or not holding of $x$, but it is also an object. Some predicates are being taken to be objects. Some cannot be so taken, the index example being non-self-membership. Quine's adoption of this criterion was purely pragmatic. We believe that there may be a way to motivate it which preserves the impression that it might be a logical notion. We need a reason to believe that the stratification criterion picks out those predicates which are ``genuine'' in some sense. We have elsewhere suggested such a motivation, based on the idea that stratified predicates are those which are invariant in a suitable sense under redefinitions of the membership relation by permutation...the underlying idea being that the identification of predicates with particular objects required to implement membership is extrinsic to the predicates and to the objects, and that genuine properties of objects should be invariant under redefinition of membership. There is also the original view which probably accurately represents Quine's thinking: logic of order $\omega$ is logic. Then the collapse of the types into one can be evaluated as a pragmatic move to simplify matters, still leaving us with an implementation of logic of order $\omega$, though incidentally creating more predicates which we cannot (or at least do not) reify. The second is whether we should at the same time introduce other related notions, such as abstract relations or functions (for which pairs are useful). In the domain of first order logic we did this, but Quine's working set of concepts includes all of the ones we used. We have not so far chosen to implement relational or functional abstraction directly in this system [though we did implement lambda terms, and also pairs and their projections, as primitives in previous versions of Marcel]. So far we are choosing to keep membership and set abstraction as our primitives. Quine did not take set abstraction as primitive: he defined set abstraction as a species of definite description, and used a contextual definition of definite description, following Russell. We note that we can define (stratified) definite description using set abstraction. What we {\em have\/} done is provided a systematic way to introduce defined notions (with both term and formula values); we aim for a reasonably fluent treatment of pairs, relations and functions without introducing new primitive constructions. It is an adventure. We are letting the logic of this prover be New Foundations. In earlier versions of Marcel, we implemented NFU; the original motivation was to implement Marcel Crabb\'e's sequent calculus SF for stratified set theory with no extensionality at all but with a set abstraction construction, for which he was able to prove cut elimination. New Foundations is very convenient in certain ways. We do want to bear in mind how the logic could be weakened to NFU, and how the development of a body of mathematics would change. The mathematical project we have in mind is to carry out Specker's proof of the ``Axiom'' of Infinity in NF. This will involve developing arithmetic, which is always interesting. \section{The code} The initial utilities handle things to do with scripting. Marcel generates a Python script which will repeat a session, if prompted correctly. \begin{verbatim} ''' logfilename="testlog,txt" logfile=open(logfilename,'a') # USER COMMAND # set the log file to be used. def setlog(s): global logfilename global logfile logfile.close() logfilename="logs/"+s+'logfile.py' logfile=open(logfilename,'w') logfile.write('from graph2 import *\n\n') def usercommand(s): if demostate==True: print(s) logfile.write(s) r''' \end{verbatim} \subsection{The term and formula types} The primitive relations of the implemented theory are equality {\tt =} and membership {\tt e}. The logical connectives are the usual conjunction ({\tt \&}), disjunction ({\tt V}), implication ({\tt >}) and biconditional ({\tt X}). Implication and biconditional are displayed in the more familiar looking forms {\tt ->} and {\tt ==}. Negation ({\tt $\sim$}) is a basic construction in the formula type. The quantifiers are the usual universal ({\tt A}) and existential ({\tt E}) quantifiers. There is a construction for defined predicates to be discussed later. Terms are either variables (single lower case letters possibly followed by one or more primes {\tt `} or {\tt *}), set abstracts, or defined terms, to be discussed later. There is a much more complete discussion of the language of Marcel below. \begin{verbatim} ''' relations = ["e","="] def isrelation(s): return s in relations connectives = ["&","V",">","X"] # < is implication and X is biconditional def isconnective(s): return s in connectives # this function changes the shape of some connectives in the display. def cexp(s): if s==">": return "->" if s=="X": return "==" return s quantifiers = ["A","E"] def isquantifier(s): return s in quantifiers # we could add more primes to diversify the variables. # Actually, digits could play this role. primes = ["'","*"] def isprime(s): return s in primes # other components we might want would be pairs, lambda terms. def isformula(L): if len(L)==0: return False #atomic formula if isrelation(L[0]) and isterm(L[1]) and isterm(L[2]): return True #negation if L[0] == "~" and isformula(L[1]):return True #binary propositional connective if (isconnective(L[0]) and isformula(L[1]) and isformula(L[2])): return True #quantified formula if (isquantifier(L[0]) and type(L[1]) == str and type(L[2]) == int and isformula(L[3])): return True # formula let terms look typgraphically the same as term let terms: # what this does is force formula definitions to have arguments) # we allow defined constant terms but not defined constant formulas # let term if L[0] == "let" and isterm(L): return True return False # isterm does not do a stratification check. Does it need to? def isterm(L): if len(L)==0: return False #variable if (L[0] == "var" and type(L[1]) == str and type(L[2]) == int): return True #set abstract if (L[0] == "set" and type(L[1]) == str and type(L[2]) == int and isformula(L[3])): return True #defined if L[0] == "defined" and type(L[1]) == str: return True #let term if (L[0] == "let" and isterm(L[1]) and L[1][0]=="var" and isterm(L[2]) and isterm(L[3]) and (L[3][0]=="defined" or L[3][0]=="let")): return True return False r''' \end{verbatim} An important but invisible feature of term and formula management in the prover is occurrence indexing of variables. Each occurrence of a variable has a different index, except that variables bound by the same quantifier or set abstract are identified as the same occurrence. It is occurrences, not variables per se, that are assigned relative type in the stratification algorithm. Free occurrences of a variable, though they are all differently indexed as occurrences, in fact represent the same object. Occurrence indices are not displayed. The functions below are used to renumber occurrences indices of variables bound by the same binder so that they are the same: the intended condition is that this is the {\em only\/} situation in which occurrence indices of variables are the same. \begin{verbatim} ''' # these functions are used to renumber occurrences # of variables which are bound # by the same quantifier or abstract: # such occurrences are identified. def reinstt(s,n,L): if (L[0]=="var" and L[1] == s and type(L[2])==int): return [L[0],L[1],n] if (L[0]=="var" and type(L[1])==str and type (L[2])==int):return L if (L[0]=="set" and L[1] == s and type(L[2])==int and isformula(L[3])): return L if (L[0]=="set" and type(L[1])==str and type (L[2])==int and isformula (L[3])): return [L[0],L[1],L[2], reinstf(s,n,L[3])] if L[0]=="defined": return L if L[0]=="let": return [L[0],L[1], reinstt(s,n,L[2]), reinstt(s,n,L[3])] return "!!!" def reinstf(s,n,L): if (isrelation(L[0]) and isterm(L[1]) and isterm(L[2])): return [L[0],reinstt(s,n,L[1]) ,reinstt(s,n,L[2])] if L[0]=="~" and isformula(L[1]): return [L[0],reinstf(s,n,L[1])] if (isconnective(L[0]) and isformula(L[1]) and isformula(L[2])): return [L[0],reinstf(s,n,L[1]) ,reinstf(s,n,L[2])] if (isquantifier(L[0]) and L[1]==s and type(L[2])== int and isformula(L[3])): return L if (isquantifier(L[0]) and type(L[1])==str and type(L[2])==int and isformula(L[3])): return [L[0],L[1],L[2], reinstf(s,n,L[3])] if L[0]=="let": return [L[0],L[1], reinstt(s,n,L[2]), reinstt(s,n,L[3])] # term function in the formula # third argument is not a mistake return "???" r''' \end{verbatim} \subsection{Display functions and parser} For ease of prototyping, the display notation and the input notation of this prover are (at least up to this point) quite different. Terms and formulas are input in Polish notation and output in a rather more familiar looking style. We describe the language of the prover, in standard mathematical terms and in terms of input and output. Formulas are as follows \begin{itemize} \item Atomic formulas are identity statements and membership statements. If $t$ and $u$ are terms, the mathematical notations are $t=u$, $t \in u$ for identity and membership statements respectively. The input notations are {\tt =tu}, {\tt etu} (where $t$ and $u$ are expressed in input notation). The output notations are {\tt t = u} and ${\tt t \, e \, u}$ respectively (where $t$ and $u$ are expressed in output notation). \item The binary propositional connectives are conjunction, disjunction, implication and biconditional. Where $p$ and $q$ are formulas, $(p \wedge q)$, $(p \vee q)$, $(p \rightarrow q)$ and $(p \leftrightarrow q)$ are the respective mathematical notations, implemented as input by {\tt \&pq}, {\tt Vpq}, {\tt >pq}, {\tt Xpq} and as output by\newline {\tt (p \& q)}, {\tt (p V q)}, {\tt (p -> q)}, {\tt (p == q)}. \item Negation is a separate construction because of arity. Where $p$ is a formula, $\neg p$ is its negation, with input and output notation {\tt $\sim$p}. \item Quantified formulas are of the usual forms $(\forall x.\phi)$, $(\exists x.\phi)$, for which input notation is {\tt Ax$\phi$} and {\tt Ex$\phi$} and output notation is {\tt (Ax : $\phi$)} and \newline {\tt (Ex : $\phi$)} where {\tt x} is a variable and $\phi$ is a formula. \item A notation abbreviating a formula or term is either a capital letter $X$ or of one of the forms $K'$ or $K^*$ where $K$ is a notation abbreviating a term or formula. The input notation is {\tt X}, {\tt `K}, {\tt *K} and the output notation is {\tt X}, {\tt K'}. {\tt K*}. The same notation may serve as a term defined notion and a formula defined notion independently. A defined formula is either of the form $K[t/a]$ or $\Delta[t/a]$, where $K$ is a notation abbreviating a formula, $a$ is a variable (normally appearing in $K$), $t$ is a term, and $K[t/a]$ represents the result of replacing $a$ with $t$ in the formula abbreviated by $K$, and $\Delta[t/a]$ represents the result of replacing $a$ with $t$ in the expanded version of the defined formula $\Delta$. The namespaces of variables used in defined notions $K$ and in the ordinary language of the prover are disjoint though the surface notations for the variables are the same (we will see how this is implemented). The input notation for this is {\tt :atK}, resp. {\tt :at$\Delta$}. The output notation is {\tt K(a:t)}, resp. {\tt $\Delta$(a:t)}. A convenient exception in the output notation is that {\tt :at:bu$\Delta$} expands as {\tt (t $\Delta$ u)}, where the keys are literally {\tt a} and {\tt b}. \end{itemize} Terms are as follows: \begin{itemize} \item Variables are lower case letters, possibly differentiated with primes. A variable is either {\tt x} (any lower case letter) or $v'$ or $v^*$ where $v$ is a variable. The input notation is {\tt x}, {\tt `v}, {\tt *v} [sorry, but this lets the Polish notation work cleanly] and the output notation is the more sensible {\tt x}, {\tt v'}, {\tt v*}. Fresh variables introduced by the quantifier rules are suffixed with {\tt !} (arbitrary variables) or {\tt ?} (unknown variables, which can later be set to specific values). These suffixes are not understood by the parser. The parser will not allow a variable which has been used as a fresh variable to be bound. The user should be warned that there are contexts in user commands where variables are entered in output notation (without any {\tt !} or {\tt ?}). There are additional variables {\tt @v} which cannot be input by the user (generated by expansion of definitions or use of theorems): they can be addressed with some commands using their output notation. There are internal variables {\tt \#v} used in the innards of the definition feature which should never be seen by the user. Variables have occurrence indices which are managed by the prover and never seen by the user. Two occurrences of a variable have the same occurrence index precisely if they are bound by the same binder (quantifier or set abstraction). \item Set abstracts are of the form $\{v \mid \phi\}$ where $\phi$ is a formula and $v$ is a variable. The input notation is {\tt \{v$\phi$} and the output notation is {\tt \{v | $\phi$\}}. It is useful to note that the parser will not accept set abstracts which are not stratified [in a weak sense to be described]. \item A defined term is either of the form $K$ or $\Delta[t/a]$, where $K$ is a notation abbreviating a term [defined above in the clause on defined formulas], $a$ is a variable (normally appearing in the term represented by $K$), $t$ is a term, and $\Delta[t/a]$ represents the result of replacing $a$ with $t$ in the expanded version of the defined term $\Delta$. The namespaces of variables used in defined notions $K$ and in the ordinary language of the prover are disjoint (we will see how this is implemented). The input notation for this is {\tt K}, resp. {\tt :at$\Delta$}. The output notation is {\tt K}, resp. {\tt $\Delta$(a:t)}. A convenient exception in the output notation is that {\tt :at:bu$\Delta$} expands as {\tt (t $\Delta$ u)}, where the keys are literally {\tt a} and {\tt b}. Note that all defined formulas are typographically identical to defined terms, a fact which the prover takes advantage of in various places. The same notation can be used to denote a defined term and an (obviously different) defined formula. Use of notations without substitutions for formulas is excluded because a need for these is not seen, and there are other uses of capital letters initial to input notations for formulas. \end{itemize} A new feature: the form {\tt .tu} abbreviates {\tt :atu} while {\tt.t.uv} abbreviates {\tt :at:buv}, {\tt.t.u.vw} abbreviates {\tt :at:bu:cvw} and so forth. This works for both terms and formulas. \begin{verbatim} ''' # display functions # the display of terms highlights things #which might be "fresh variables" # introduced by the quantifier rules, # though it doesn't test whether they are free # (the parser has now been changed so that # fresh variables cannot be bound, even apparently: # no bound variable can have the same surface form). # added infix display of let terms (for both terms and formulas) # if the first two keys used are a and b # function to insert line breaks # to avoid margin overflow. The criterion is # a bit weird. def maybebreak(L,M): if ((len(str(L))>25 and len(str(M))> 60) or (len(str(M))>25 and len(str(L))> 60)): return "\n " return " " def displayf(L): global unknowns global freshvars if (isrelation(L[0]) and isterm(L[1]) and isterm(L[2])): return ((displayt(L[1])) +(maybebreak(L[1],L[2])) +L[0]+" "+(displayt(L[2]))) if L[0] == "~" and isformula(L[1]): return "~" + (displayf(L[1])) if (isconnective(L[0]) and isformula(L[1]) and isformula(L[2])): return ("("+(displayf(L[1])) +(maybebreak(L[1],L[2])) +cexp(L[0])+" "+(displayf(L[2]))+")") if (isquantifier(L[0]) and type(L[1])==str and type(L[2]) == int and isformula(L[3])): return ("("+L[0]+L[1]+" : " +(displayf(L[3]))+")") if L[0]=="defined" and type(L[1]) == str: return L[1] if (L[0]=="let" and isterm(L[1]) and L[1][0]=="var" and L[1][1]=="a" and isterm(L[2]) and L[3][0]=="let" and isterm(L[3][1]) and L[3][1][0]=="var" and L[3][1][1]=="b" and isterm(L[3][2]) and isterm(L[3][3])): return ("("+(displayt(L[2])) +" "+(displayf(L[3][3])) +" "+(displayt(L[3][2]))+")") if (L[0]=="let" and isterm(L[1]) and L[1][0]=="var" and isterm(L[2]) and isterm(L[3]) and (L[3][0]=="defined" or L[3][0]=="let")): return (displayt(L[3])+"("+displayt(L[1]) +":"+displayt(L[2])+")") return "???" def displayt(L): global unknowns global freshvars if (L[0]=="var" and not(findunknown(L[1])=="error")): return L[1]+"?" if L[0]=="var" and L[1] in freshvars: return L[1]+"!" if (L[0]=="var" and type(L[1]) == str and type(L[2]) == int): return L[1] if L[0]=="defined" and type(L[1]) == str: return L[1] if (L[0]=="let" and isterm(L[1]) and L[1][0]=="var" and L[1][1]=="a" and isterm(L[2]) and L[3][0]=="let" and isterm(L[3][1]) and L[3][1][0]=="var" and L[3][1][1]=="b" and isterm(L[3][2]) and isterm(L[3][3])): return ("("+(displayt(L[2])) +(maybebreak(L[2],L[3][2])) +(displayt(L[3][3])) +" "+(displayt(L[3][2]))+")") if (L[0]=="let" and isterm(L[1]) and L[1][0]=="var" and isterm(L[2]) and isterm(L[3]) and (L[3][0]=="defined" or L[3][0]=="let")): return (displayt(L[3])+"("+displayt(L[1]) +":"+displayt(L[2])+")") if (L[0]=="set" and type(L[1]) == str and type(L[2]) == int and isformula(L[3])): return "{"+L[1]+" | "+(displayf(L[3]))+"}" return "!!!" # parser newint = 1 def shownewint(): print(newint) # note that the parser enforces #stratification of set abstract terms. # However, it does this in quite a weak sense. # Types are assigned # to occurrences of variables, # not to variables themselves; the only # occurrences which are identified # are those bound by the same abstract # or quantifier. Further, the #stratification test for abstracts only # checks variables which are connected # to the variable bound in the abstract. # this is all that is necessary; # it is even less than Marcel's weak # stratification criterion. # the list of all variables used variables=[] def showvariables(): print(variables) # the list of all "unknowns" # (witnesses introduced for later specification) unknowns=[] def showunknowns(): print(unknowns) # the list of all fresh variables # (arbitraries and unknowns) introduced by quantifier rules freshvars=[] def showfreshvars(): print(freshvars) # The parser: for rapid prototyping, # this is Polish notation. # The display notation is more standard. # Examples when they are produced # will give an indication of # how to enter terms and formulas. # Weak stratification checking # of set abstracts is done at parse time. # The graph generation # and stratification functions are below. def isspace(s): return (s==" " or s=="(" or s == ")" or s == "[" or s == "]" or s ==",") # these allow organization of the Polish notation input def applyprime(p,L): if len(L)==0: return "!!!" return [L[0]]+[L[1]+p]+L[2:] # this makes it possible to prime both variables and definienda. def raisekey(t): if t[0]=="let" and len(t[1][1])==1: return ["let",gett(chr(ord(t[1][1])+1)),t[2],raisekey(t[3])] return t def gett(s): global newint global variables if len(s)==0: return "!!!" if isspace(s[0]): return gett(s[1:]) if isprime(s[0]): v=applyprime(s[0],gett(s[1:])) if v == "!!!": return "!!!" if (("a" <= v[1][0] and v[1][0] <= "z") and not(v[1] in variables)): variables=variables+[v[1]] return v if "a" <= s[0] and s[0] <= "z": if not(s[0] in variables): variables=variables+[s[0]] newint=newint+1 return ["var",s[0],newint] if (("A" <= s[0] and s[0] <= "Z") or ("0" <= s[0] and s[0] <= "9")): return ["defined",s[0]] if s[0]==":": V=gett(s[1:]) T=gett(restt(s[1:])) B=gett(restt(restt(s[1:]))) if not(V[0]=="var"): return "!!!" if (not(B[0]=="defined" or B[0]=="let")): return "!!!" return ["let",V,T,B] if s[0]==".": T=gett(s[1:]) B=gett(restt(s[1:])) if (not(B[0]=="defined" or B[0]=="let")): return "!!!" return ["let",gett("a"),T,raisekey(B)] if s[0]=="{": var=gett(s[1:]) if not (var[0]=="var"): return "!!!" if var[1] in freshvars: print("Attempt to bind a fresh variable") return "!!!" FF= getf(restt(s[1:])) if not(isformula(FF)): return "!!!" F=reinstf(var[1],var[2],FF) S=stratify(graphf(F),[var[1],var[2]]) if S[0]=="stratification failure": print(displayf(F)) print(S) return "bad set abstract" return ["set",var[1],var[2],F] return "!!!" def restt(s): if len(s)==0: return "" if isspace(s[0]): return restt(s[1:]) #if s[0]=="#": return restt(s[1:]) if isprime(s[0]): return restt(s[1:]) if "a"<=s[0] and s[0]<="z": return s[1:] if (("A"<=s[0] and s[0]<="Z") or ("0" <= s[0] and s[0] <= "9")): return s[1:] if s[0]==":": return restt(restt(restt(s[1:]))) if s[0]==".": return restt(restt(s[1:])) if s[0]=="{": var=gett(s[1:]) if not(var[0]=="var"): return "" return restf(restt(s[1:])) return "" def getf(s): global newint global variables if len(s)==0: return "???" if isspace(s[0]): return getf(s[1:]) if len(s)==0:return "???" if isrelation(s[0]): return [s[0],gett(s[1:]),gett(restt(s[1:]))] if s[0]=="~":return [s[0],getf(s[1:])] if isconnective(s[0]): return [s[0],getf(s[1:]),getf(restf(s[1:]))] if isquantifier(s[0]): var=gett(s[1:]) if not (var[0]=="var"): return "???" return [s[0],var[1],var[2], reinstf(var[1],var[2], getf(restt(s[1:])))] if s[0]==":" or s[0]==".": return gett(s) # getting a term here is a trick; # let terms have same form in both classes, and in this way # we forbid defined formulas without assignments to arguments. return "???" def restf(s): if len(s)==0:return "???" if isspace(s[0]):return restf(s[1:]) if isrelation(s[0]): return restt(restt(s[1:])) if s[0]=="~":return restf(s[1:]) if isconnective(s[0]):return restf(restf(s[1:])) if isquantifier(s[0]): var=gett(s[1:]) if not(var[0]=="var"): return "" return restf(restt(s[1:])) if s[0]==":": return restt(s) return "" def testt(s):return displayt(gett(s)) def testf(s):return displayf(getf(s)) r''' \end{verbatim} \subsection{Substitution functions} In this block of code various kinds of substitution are addressed. There are two kinds of substitution that are made: one is replacement of all occurrences of variables bound by a particular binder [so here we are actually replacing an occurrence, and its index is part of the data supplied], and one is replacement of all free occurrences of variables in a context [occurrence index not relevant]. In all kinds of substitution, the term replacing the variable has its occurrence indices displaced out of the range of indices already used, separately for each time the term is substituted in. This enforces the fact that occurrences of variables are identified exactly if they are bounded by the same binder. Notice that the displacement mechanism preserves identity of occurrences bound in the substituted term by the same binder. There is also a mechanism for replacing a term uniformly by a variable where it occurs, used by higher order matching. The function for generating a variable with a new name is included here. This is a good time to notice a strange feature of this prover. It takes no visible precautions against bound variable capture. Substitution of a free variable into a binding scope with the same shape as the binding variable is possible (though deviously), but the prover will not be confused, because of the invisible occurrence indices. Probably I ought to do something about this. \begin{verbatim} ''' # the range of occurrence indices in a term or formula # needed for substitution # I need to think about what # to do with expressions which actually have # no variables in them, # possible if we have defined constants. def occt(t): if t[0]=="var": return [t[2],t[2]] if t[0]=="set": R=occf(t[3]) return [min(t[2],R[0]),max(t[2],R[1])] if t[0]=="let" and t[3][0]=="defined": return occt(t[2]) if t[0]=="let": return occt(t[2]) return [newint,newint] def occf(f): if isrelation(f[0]): a=occt(f[1]) b=occt(f[2]) if f[1][0]=="defined": return b if f[2][0]=="defined": return a return [min(a[0],b[0]),max(a[0],b[0])] if f[0]=="~": return occf(f[1]) if isconnective(f[0]): a=occf(f[1]) b=occf(f[2]) return [min(a[0],b[0]),max(a[0],b[0])] if isquantifier(f[0]): a=occf(f[3]) return [min(f[2],a[0]),max(f[2],a[1])] if f[0]=="let" and f[3][0]=="defined": return occt(f[2]) if f[0]=="let": return occt(f[2])+occt(f[3]) #use of occt is not an error return [newint,newint] #this is hard substitution for variable occurrences. # The same copy is put in everywhere (with occurrences refreshed). #this preserves stratification. I am not sure whether # soft substitution based just on surface form of variables is needed at all. #probably it is, but it should be used sparingly. (setunknown uses it). #amusingly, this has no compensation # for bound variable collision because # (though it can *look* as if it happens) it doesnt. #but there should be a display function tweak #to highlight apparent bound variable collisions. (there isnt yet.) # these functions compute the range of occurrence indices in a term, # so that substitution knows how far up to displace occurrence indices # when substituting a term into a context, and how much to increase nextint # (the variable containing the next occurrence index) # start here, working on definition syntax def displaceocct(t,d): if t[0] == "var": return ["var",t[1],t[2]+d] if t[0] == "set": return ["set",t[1],t[2]+d, displaceoccf(t[3],d)] if t[0] == "let": return ["let", t[1], displaceocct(t[2],d), displaceocct(t[3],d)] if t[0] == "defined": return t def displaceoccf(f,d): if isrelation(f[0]): return [f[0], displaceocct(f[1],d), displaceocct(f[2],d)] if f[0]=="~": return ["~", displaceoccf(f[1],d)] if isconnective(f[0]): return [f[0], displaceoccf(f[1],d), displaceoccf(f[2],d)] if isquantifier(f[0]): return [f[0],f[1],f[2]+d, displaceoccf(f[3],d)] if f[0] == "let": return ["let", f[1], displaceocct(f[2],d), displaceocct(f[3],d)] # substitution without displacement # for a variable with a precise occurrence # index (as with a bound variable) def subs1t(v,n,t,u): if u == ["var",v,n]: return t if u[0]=="var": return u if (u[0]=="set" and u[1]==v and u[2]==n): return u if u[0]=="set": return ["set",u[1],u[2], subs1f(v,n,t,u[3])] if u[0]=="defined": return u if u[0]== "let": return ["let",u[1], subs1t(v,n,t,u[2]), subs1t(v,n,t,u[3])] def subs1f(v,n,t,u): if isrelation(u[0]): return [u[0], subs1t(v,n,t,u[1]), subs1t(v,n,t,u[2])] if u[0]=="~": return ["~",subs1f(v,n,t,u[1])] if isconnective(u[0]): return [u[0], subs1f(v,n,t,u[1]), subs1f(v,n,t,u[2])] if (isquantifier(u[0]) and u[1]==v and u[2]==n): return u if isquantifier(u[0]): return [u[0],u[1],u[2], subs1f(v,n,t,u[3])] if u[0]== "let": return ["let",u[1], subs1t(v,n,t,u[2]), subs1t(v,n,t,u[3])] # substitution without displacement # (soft) for a free variable # it is used by commands # for global substitution into proofs, which # supply the needed displacement # of the substituted text. # added fresh displacement # in each substitution. This removes # a technical stratification problem. def freesubs1t(v,t,u): global newint if u[0]=="var" and u[1]==v: a=occt(t) d=newint-a[0]+1 newint=a[1]+d T=displaceocct(t,d) return T if u[0]=="var": return u if u[0]=="set" and u[1]==v: return u if u[0]=="set": return ["set",u[1],u[2], freesubs1f(v,t,u[3])] if u[0]=="defined": return u if u[0]== "let": return ["let",u[1], freesubs1t(v,t,u[2]), freesubs1t(v,t,u[3])] def freesubs1f(v,t,u): if isrelation(u[0]): return [u[0], freesubs1t(v,t,u[1]), freesubs1t(v,t,u[2])] if u[0]=="~": return ["~",freesubs1f(v,t,u[1])] if isconnective(u[0]): return [u[0], freesubs1f(v,t,u[1]), freesubs1f(v,t,u[2])] if isquantifier(u[0]) and u[1]==v: return u if isquantifier(u[0]): return [u[0],u[1],u[2], freesubs1f(v,t,u[3])] if u[0]== "let": return ["let",u[1], freesubs1t(v,t,u[2]), freesubs1t(v,t,u[3])] #these are the real (hard) substitution functions: #the substituted text has all its occurrence indices made fresh, so # nothing in it cannot be bound by something outside it, #and no stratification problems can be introduced # if the original formula was weakly stratified # in our very weak sense. # it feels really weird to write a substitution function #which completely ignores the variable capture problem. # probably the display function should alert the user #about apparently captured variables. But this might actually # be expensive. # the only user command which would cause apparent variable capture is # setunknown, and so far I havent installed any warning. I should do # a test that it actually behaves as I expect. (Not true, one can use # the membership sequent rules to demonstrate apparent variable capture). # Apparent variable capture is a thing, and to all appearances #the system behaves correctly; it doesnt *show* # you the occurrence data. def subst(v,n,t,u): global newint a=occt(t) d=newint-a[0]+1 newint=a[1]+d T=displaceocct(t,d) return subs1t(v,n,T,u) def subsf(v,n,t,u): global newint a=occt(t) d=newint-a[0]+1 newint=a[1]+d T=displaceocct(t,d) return subs1f(v,n,T,u) def raisef(f): global newint a=occf(f) d=newint-a[0]+1 newint=a[1]+d F=displaceoccf(f,d) return F # functions for changing variable names to fresh names. # new names will be generated using priming if necessary. def dropitem(v,L): if L==[]: return [] if L[0]==v: return dropitem(v,L[1:]) return [L[0]]+dropitem(v,L[1:]) # this function makes the generation of fresh variables much # less cluttering. In effect, binary notation in the primes ' and * def nextvarname(s): if s[0]=="#" or s[0]=="@": return nextvarname(s[1:]) if s[-1]=="'": return s[0:-1]+"*" if s[-1]=="*": return (nextvarname(s[0:-1]))+"'" return s+"'" # this simple function completely replaces renamevar* def newvariable(v): global variables if v[1] in variables: return newvariable(["var", nextvarname(v[1]),v[2]]) variables=variables+[v[1]] return v def newvariable2(v): global variables if v[1] in variables: return newvariable2(["var", nextvarname(v[1]),v[2]]) #variables=variables+[v[1]] return v # this is the complicated term renaming case needed for # higher order matching. In the term t, the term v is replaced with the # new variable w. It has a peculiar name due to the history of the code. def renamevart2a(v,w,t): global variables if (w[1] in variables): return renamevart2(v,newvariable2(w),t) if (v[0]=="var" and t[0]== "var" and t[1]==v[1]): return [w,w] if (not(v[0]=="var") and ((not(t[0]=="var")) or (t[0]=="var" and findunknown(t[1])=="error") and equalt(v,t))): return [w,w] if t[0]=="var": return [t,w] if (t[0]=="set" and v[0]=="var" and t[1]==v[1]): return [t,w] if t[0]=="set": return [["set",t[0],t[1], renamevarf2a(v,w,t[3])[0]],w] if t[0]=="defined": return [t,w] if t[0]=="let": return [["let",t[1], renamevart2a(v,w,t[2]), renamevart2a(v,w,t[3])],w] def renamevarf2a(v,w,f): global variables if (w[1] in variables): return renamevarf2(v,newvariable2(w),f) if isrelation(f[0]): return[[f[0], renamevart2a(v,w,f[1])[0], renamevart2a(v,w,f[2])[0]],w] if f[0]=="~": return [[f[0], renamevarf2a(v,w,f[1])[0]],w] if isconnective(f[0]): return[[f[0], renamevarf2a(v,w,f[1])[0], renamevarf2a(v,w,f[2])[0]],w] if (isquantifier(f[0]) and v[0] == "var" and f[1]==v[1]): return [f,w] if isquantifier(f[0]): return [[f[0],f[1],f[2], renamevarf2a(v,w,f[3])[0]],w] if f[0]=="let": return [["let",f[1], renamevart2a(v,w,f[2]), renamevart2a(v,w,f[3])],w] def renamevart2(v,w,t): global variables global newint newint=newint+1 w=["var",w[1],newint] R=renamevart2a(v,w,t) variables = variables+[w] return R def renamevarf2(v,w,t): global variables global newint newint=newint+1 w=["var",w[1],newint] R=renamevarf2a(v,w,t) variables = variables+[w] return R r''' \end{verbatim} \subsection{The graph based stratification algorithm} The stratification checker proceeds by first building a weighted directed graph involving all occurrences of variables in the term or formula and base nodes generated for each term involved. The graph for an atomic sentence has edges in both directions with weights appropriate for the relations: if the formula is $t=u$ the graph consists of the graph for $t$, the graph for $u$, and weight 0 edges in both directions between their base nodes. If the formula is $t \in u$ the graph consists of the graph for $t$, the graph for $u$, and edges between the base nodes of weight 1 from $t$ to $u$ and $-1$ from $u$ to $t$. Graphs for logically connected and quantified sentences are simply graphs of appropriate subformulas or in the case of binary connectives the union of two graphs. The graphs for defined formulas are computed by computing the graphs for terms substituted in then linking their base nodes with weights determined by comparing the types of the keys for which they are substituted. Defined terms and formulas are required to be uniquely typed (up to uniform displacement): they have to be not just stratified but connected. The graph for a variable has a base node with weight 0 links in both directions to the variable occurrence. The graph for a set $\{x\mid \phi\}$ has graph consisting of the graph for $\phi$ with a base node with a weight $1$ link from the bound occurrence of $x$ and a weight $-1$ link to the bound occurrence of $x$. The graph for a defined term consists of graphs for terms substituted in with links from base nodes of those terms to the base node of the whole term and back with weights determined by the types of the keys in the definition relative to the type of the whole term defined. The condition for stratification is simple: for any two nodes in the graph, there is at most one length for a path between them (the length of a path being the sum of the weights of the edges in it). The existence of a cycle of nonzero length is exactly equivalent to failure of stratification. The algorithm used is similar to Dijkstra's algorithm. Choose a starting point in the graph (in the case of a term, this will be the base node). Set the distance from the starting node to itself to 0 and all other distances to $\infty$. When we process a node $v$ which has a finite distance from the starting node, we use each edge from $v$ to a node $w$ to compute a distance from the starting node to $w$. If the distance to $w$ was heretofore infinite, correct it and record a path from the starting node to $w$. If the distance to $w$ was heretofore finite and the new estimate agrees with it exactly, do nothing. If it disagrees, report failure of stratification and construct a cycle of nonzero length to report as data with the stratification failure conclusion. In the master algorithm we process each term with finite distance from the starting node once, and we stop when there are no more nodes with finite distance and report a distance function, if no failure of stratification has occurred. The criterion for stratification here is that each variable occurrence which is connected to the starting variable (which may be taken to be the binding variable in a set abstract) is assigned a consistent finite type. Note that different occurrences of free variables may be assigned different types. The parser tests set abstracts and does not even allow unstratified ones to be displayed. The definition facility requires that the body of a definition be stratified and that no node be at infinite distance from the starting point (stratified and connected), and further that variables of the same shape, even if free, are always assigned the same type independent of occurrence index (so quite rigidly stratified). \begin{verbatim} ''' # constructing the graph from a formula def addkey(s,x,L): if L==[]:return [[s,[x]]] if L[0][0]==s:return [[L[0][0],[x]+L[0][1]]]+L[1:] return [L[0]]+(addkey(s,x,L[1:])) # I have done easy tests of stratification, but a full test of # the type differentials involving set abstracts is probably a good idea. def graphf(L): global countbase startgraph=[] if isrelation(L[0]) and isterm(L[1]) and isterm(L[2]): c1=[str(countbase+1),-1] G1=grapht(L[1]) c2=[str(countbase+1),-1] G2=grapht(L[2]) startgraph=(G1+G2) if L[0]=="=": startgraph=addkey(c1,[c1,c2,0],startgraph) startgraph=addkey(c2,[c2,c1,0],startgraph) if L[0]=="e": startgraph=addkey(c1,[c1,c2,1],startgraph) startgraph=addkey(c2,[c2,c1,-1],startgraph) return startgraph if L[0]=="~": return graphf(L[1]) if isconnective(L[0]): return (graphf(L[1]) +graphf(L[2])) if isquantifier(L[0]): return graphf(L[3]) if L[0]=="let" and L[3][0]=="defined": thedefquery=findvalues(L[3][1],formuladefs) if thedefquery==[]: print ("undefined definition formula") startgraph= addkey([basename,-1], [[basename,-1], [basename,-1],1], startgraph) return startgraph thetypes=thedefquery[0][1] thetypequery=findvalues(L[1][1],thetypes) if thetypequery==[]: print ("no type for this variable found") startgraph= addkey([basename,-1], [[basename,-1], [basename,-1],1], startgraph) return startgraph thetype=thetypequery[0] countbase=countbase+1 c2=[str(countbase),-1] c1=[str(countbase+1),-1] G1=grapht(L[2]) startgraph=G1 startgraph=addkey(c2,[c2,c1,thetype], startgraph) startgraph=addkey(c1,[c1,c2,-thetype], startgraph) return startgraph if L[0]=="let": search=L[3] while(not(search[0]=="defined")): search=search[3] thedefquery=findvalues(search[1],formuladefs) if thedefquery==[]: print ("undefined definition term") startgraph= addkey([basename,-1], [[basename,-1], [basename,-1],1], startgraph) return startgraph thetypes=thedefquery[0][1] thetypequery=findvalues(L[1][1],thetypes) if thetypequery==[]: print ("no type for this variable found") startgraph= addkey([basename,-1], [[basename,-1], [basename,-1],1], startgraph) return startgraph thetype=thetypequery[0] c2=[str(countbase+1),-1] G2=graphf(L[3]) c1=[str(countbase+1),-1] G1=grapht(L[2]) startgraph=G1+G2 startgraph=addkey(c2,[c2,c1,thetype], startgraph) startgraph=addkey(c1,[c1,c2,-thetype], startgraph) return startgraph return [] # adding in a node [base,-1] standing for the term itself in grapht # this means there are lots of base nodes generated, one for every subterm! def grapht0(L,basename): startgraph=[] if L[0]=="var": startgraph=addkey([basename,-1], [[basename,-1], [L[1],L[2]],0], startgraph) startgraph=addkey([L[1],L[2]], [[L[1],L[2]], [basename,-1],0], startgraph) return startgraph if L[0]=="set": startgraph=graphf(L[3]) startgraph=addkey([basename,-1], [[basename,-1], [L[1],L[2]],-1], startgraph) startgraph=addkey([L[1],L[2]], [[L[1],L[2]], [basename,-1],1], startgraph) return startgraph if L[0]=="defined": startgraph=[] startgraph=addkey([basename,-1], [[basename,-1], [basename,-1],0], startgraph) return startgraph if L[0]=="let": c1=[basename,-1] G1=grapht0(L[3],basename) c2=[str(countbase+1),-1] G2=grapht(L[2]) startgraph = G1+G2 search=L[3] while(not(search[0]=="defined")): search=search[3] thedefquery=findvalues(search[1],termdefs) if thedefquery==[]: print ("undefined definition term" +(search[1])) startgraph= addkey([basename,-1], [[basename,-1], [basename,-1],1], startgraph) return startgraph thetypes=thedefquery[0][1] thetypequery=findvalues(L[1][1],thetypes) if thetypequery==[]: print ("no type for this variable found") startgraph= addkey([basename,-1], [[basename,-1], [basename,-1],1], startgraph) return startgraph thetype=thetypequery[0] startgraph=addkey(c1,[c1,c2,thetype], startgraph) startgraph=addkey(c2,[c2,c1,-thetype], startgraph) return startgraph countbase=1 def grapht(L): global countbase countbase=countbase+1 return grapht0(L,str(countbase)) # using graph method to check stratification # with the graph as input # and a starting point, compute a distance function # (a relative type assignment) from that starting point. # a distance function is a list of pairs of a vertex # and either the empty set (for infinite distance) # or a singleton of an integer, followed by # either the empty set or a path (for data # extraction) # make the initial distance table # from a given starting point def makedistances(L,x): if L==[]: return [] m=makedistances(L[1:],x) if not(getdistance(m,L[0][0])=="error"): return m if L[0][0]==x: return [[x,[0],[x]]]+m return ([[L[0][0],[],[]]] +makedistances(L[1:],x)) def makedistancet(L): return makedistances(L,L[0][0]) # get the distance from the starting point # to v (as currently estimated) def getdistance(L,v): if L==[]: return "error" if L[0][0]==v: if L[0][1]==[]:return "infty" return L[0][1][0] return getdistance(L[1:],v) #get the path from the starting point # to V (if we have one) def getpath(L,v): if L==[]: print ("error") return [] if L[0][0]==v: if L[0][2]==[]: print ("none") return [] return L[0][2] return getpath(L[1:],v) # drop the distance to v (in order to replace it) def dropkey(L,v): if L==[]: return [] if L[0][0]==v: return L[1:] return [L[0]]+dropkey(L[1:],v) # function for updating a distance function # given an edge to work with # reverse a list, needed in # updatedistances to display the bad cycle nicely def rev(L): if L==[]: return [] return rev(L[1:])+[L[0]] def rev2(L): if L==[]: return [] return rev2(L[1:]) +[rev(L[0])] def updatedistances(L,v,w,n): vdist = getdistance(L,v) if not(type(vdist)==int): return "error condition" wdist = getdistance(L,w) # if w already has a different distance estimate, #construct and return a cyle of nonzero length if not(wdist=="infty" or wdist==vdist+n): return["stratification failure", (getpath(L,v)+[[v,n,w]] +rev2(getpath(L,w)))] # if the distance estimate is new, #add it (nothing to do if no updating needed) if wdist=="infty": return ([[w,[vdist+n], getpath(L,v)+[[v,n,w]]]] +dropkey(L,w)) # this output is now a bit more readable # mod the number of new nodes. return L def stratify(G,x): #initialize the distances thedistances=makedistances(G,x) i=0 while(i