commit 4427db8f18e506b5b1ab4c23964b3f0518850a98
parent ccde1ec5e431ac13cb0028fa8a9510a41cff333e
Author: Juan F. Meleiro <juan@juanmeleiro.mat.br>
Date: Sat, 6 Jan 2024 13:35:11 -0300
Add writings and restructure dirs
Diffstat:
12 files changed, 660 insertions(+), 0 deletions(-)
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1,10 @@
+*.aux
+*.log
+*.out
+*.bcf
+*.run.xml
+*.bbl
+*.blg
+*.rubbercache
+*.toc
+*.pdf
diff --git a/vm.c b/coding/vm.c
diff --git a/writing/2023-05-30-tentative-syntax.ebnf b/writing/2023-05-30-tentative-syntax.ebnf
@@ -0,0 +1,6 @@
+context = "[" , { assumption } , "]" ;
+assumption = name , context , term , proof ;
+proof = "{" , { name , proof } , "}" ;
+term = "(" , name , term , { term } , ")" | name ;
+name = namechar , { namechar } ;
+namechar = ? any character ? - ( "[" | "]" | "{" | "}" | "(" | ")" ) ;
diff --git a/writing/all.do b/writing/all.do
@@ -0,0 +1,2 @@
+redo main.pdf
+echo DONE 1>&2
diff --git a/writing/default.pdf.do b/writing/default.pdf.do
@@ -0,0 +1,5 @@
+src="$2.tex"
+build=.tmp/$(dirname "$2")
+mkdir -p "$build" 1>&2
+xelatex -halt-on-error -interaction=nonstopmode -output-directory "$build" "$src" >&2
+cp ".tmp/$1" "$3" 1>&2
diff --git a/writing/journal/2023-11-22-declare-prove-use.lua b/writing/journal/2023-11-22-declare-prove-use.lua
@@ -0,0 +1,175 @@
+local pprint = require("pprint").pprint
+-- Possible actions:
+-- * start subcontext
+-- * declare judgment
+-- * use declared judgment
+
+function die(err, msg, ...)
+ msg = tostring(msg or err)
+ if err then
+ io.stderr:write(string.format(msg .. "\n", ...))
+ os.exit(1)
+ end
+end
+
+local test = {
+ {
+ method = "down"
+ },
+ {
+ method = "declare",
+ params = {
+ name = "cv",
+ judgment = {
+ head = "var",
+ body = {
+ {
+ head = "x"
+ }
+ }
+ }
+ }
+ },
+ {
+ method = "up"
+ },
+ {
+ method = "declare",
+ params = {
+ name = "var-wff",
+ judgment = {
+ head = "wff",
+ body = {
+ {
+ head = "x"
+ }
+ }
+ }
+ }
+ }
+}
+
+local actions = {}
+
+function actions.down(state)
+ die(state.subcontext, "Unresolved subcontext")
+ table.insert(state.theories, {})
+ return state
+end
+
+function actions.up(state)
+ state.subcontext = state.theories[#state.theories]
+ table.remove(state.theories)
+ return state
+end
+
+function pressupositions(state, judgment)
+ -- This is a rabbit hole. Where do pressupositions come from? Two
+ -- options: 1) we fix the forms of judgments and hard-code the
+ -- pressupositions; 2) we find a way for the user to create
+ -- *declaration rules* that work just like assumptions but are
+ -- only used at top-level declarations.
+ return {}
+end
+
+function actions.declare(state, params)
+ die(state.focus, "Proof in progress")
+ local assumption = {
+ name = params.name,
+ conclusion = params.judgment,
+ subcontext = state.subcontext
+ }
+ state.subcontext = nil
+ table.insert(state.theories[#state.theories], assumption)
+ state.goals = pressupositions(state, params.judgment)
+ return state
+end
+
+function prune(state)
+ while #state.focus.subgoals == 0 do
+ die(not match(state.focus.goal, state.focus.candidate), "Used assumption does not prove the goal")
+ if state.focus.goal.head == "var" then
+ -- oh boy
+ -- perform unifications
+ end
+ if state.focus.parent then
+ state.focus = state.focus.parent
+ table.remove(state.focus.subgoals)
+ else
+ table.remove(state.goals)
+ if #state.goals > 0 then
+ state.focus = state.goals[#state.goals]
+ else
+ state.focus = nil
+ end
+ return state
+ end
+ end
+ return state
+end
+
+function use(state, assumption)
+ state.focus.candidate = assumption.conclusion
+ if #assumption.subcontext > 0 then
+ for i = #candidate.subcontext, 1, -1 do
+ table.insert(state.focus.subgoals, candidate.subcontext[i])
+ state.focus.subgoals[i].parent = state.focus
+ end
+ state.focus = state.focus.subgoals[#state.focus.subgoals]
+ end
+end
+
+function actions.use(state, name)
+ die(not state.goals.focus, "Nothing to prove")
+
+ local assumption = state.assets[name]
+ die(not assumption, "No assumption under that name")
+ state = use(state, assumption)
+ state = prune(state)
+ return state
+end
+
+function interpret(program, state)
+ for _,c in ipairs(program) do
+ die(not actions[c.method], "No such action '%s'", c.method)
+ state = actions[c.method](state, c.params)
+ end
+ return state
+end
+
+function judgment2str(judg)
+ local res = judg.head
+ if judg.body then
+ res = res .. "("
+ for i = 1, #judg.body do
+ res = res .. judgment2str(judg.body[i])
+ if i < #judg.body then
+ res = res .. ","
+ end
+ end
+ res = res .. ")"
+ end
+ return res
+end
+
+function printassumption(assump, level)
+ if assump.subcontext then
+ printtheory(assump.subcontext, level + 1)
+ end
+ io.write(string.rep(" ", level) .. assump.name .. " " .. judgment2str(assump.conclusion) .. "\n")
+end
+
+function printtheory(th, level)
+ level = level or 0
+ for _,a in ipairs(th) do
+ printassumption(a, level)
+ end
+end
+
+local init = {
+ goals = {},
+ theories = {{}}
+}
+
+local bigres = interpret(test, init)
+printtheory(bigres.theories[1])
diff --git a/writing/journal/2023-11-22-declare-prove-use.tex b/writing/journal/2023-11-22-declare-prove-use.tex
@@ -0,0 +1,200 @@
+\documentclass[../main.tex]{subfiles}
+
+\begin{document}
+
+ \section{2023-11-22 Declare, prove, and use}
+
+ In the Logic of Assumptions, judgments appear under three
+ different \emph{moods}. That is, these syntactical objects wich
+ express judgments, without any commitment, can appear or be
+ refered to in places where they take on different meanings.
+
+ The three moods are those of \definiendum{declaration},
+ \definiendum{assertion}, and \definiendum{use}.
+
+ There is also an interplay between them. The three moods grant
+ rights and impose demands (under the general obligation of the
+ user to say coherent things), which involve the other moods.
+
+ It works like this:
+
+ \begin{description}
+ \item[Declare] When one declares a judgment, one is taking it
+ to be true. This can be read in a few ways. For one, it can be
+ thought of as a \emph{postulate} -- \ie, the assertion that,
+ pragmatically, from now on, we'll take that judgement to the
+ the case. On the other hand, hooking into the double meaning
+ of theories in the Logic of Assumptions, we can understand a
+ declaration as a specification of part of the interface such a
+ theory is describing -- \ie, from then on, we're talking about
+ contexts which implement this judgment.
+
+ To declare something, one must \emph{prove} its
+ pressupositions. So, here, in order to \emph{be able} to declare,
+ one \emph{is required} to prove.
+
+ \item[Proof] To prove a judgment (in a collection of contexts)
+ means to establish that context implements that judgment. Or, in
+ the dual reading, that under the assumptions from such context,
+ we can conclude the given judgment. And, since judgments are
+ hypothetical, this means one can draw the conclusion of the
+ judgment if one has its hypothesis.
+
+ Proof is impositional. One, at least intentionally speaking,
+ doesn't \emph{choose} to prove. One is \emph{required} to do
+ so. But the counterpart is this: when such imposition is made,
+ we also get the right to \emph{use} the assumptions of the
+ judgment, besides the given context. The movement is ``assume
+ the hypotheses, show the conclusion'', and so the mood of proof
+ enables the mood of use.
+
+ \item[Use] To use a judgment means to refer to it when it is
+ already established -- that is, declared. But \emph{use}, in this
+ sense, means to apply judgments as rules. That is, if we wish
+ to use the conclusion (\eg, in the course of an ongoing proof),
+ one must first \emph{prove} the hypotheses of the judgment under
+ the current context. So \emph{use} demands both \emph{proof}
+ and \emph{declaration}.
+
+ \end{description}
+
+ To summarize:
+
+ \begin{itemize}
+ \item To declare, one must prove (the pressupositions).
+ \item To prove, one \emph{can} use.
+ \item To use, one must prove (and have declared).
+ \end{itemize}
+
+ In practice, the flow of theory development is a sequence
+ of declarations. On each declaration, we prove the
+ pressupositions. And then we alternate between \emph{having to
+ prove} judgmenets, thereby enabling the use of its hypotheses,
+ and \emph{being able to use} judgments, which requires us to
+ prove its hypotheses.
+
+ \subsection{Implementation}
+
+ Let's think of the data structures needed to keep track of all these needs ands cans.
+
+ When building a theory, on the top level, we are always declaring
+ judgments. On the context, we have two structures.
+
+ The first is the \definiendum{goal tree}, which is a tree made
+ of judgments. If the tree is not empty, the root represents the
+ judgment currently being declared, and it is a \definiendum{use
+ node}. Goal nodes have zero or one child, which (if it exists)
+ represent the judgment that is being used to prove that
+ goal. The children of a used judgment are the goals that it
+ entails. Additionally, the forest has a \emph{pointer}.
+
+ The other is for \definiendum{assets}, or things which we've
+ gotten granted the right of using, and it is an assoctiation
+ list between names and judgments (with links to the places
+ in the goal tree where they were introduced).
+
+ When focusing on something to prove, or when using something,
+ those lists will be modified.
+
+ So, at any point in top-level, we've got an empty tree of
+ goals (\ie, we have a valid theory so far), and all previous
+ declarations show up as assets. Here's how states work:
+ depending on the goal tree, the user has some valid actions,
+ and each action generates some changes to the state.
+
+ \begin{tabular}{lcr}
+ Condition & Actions & Parameters \\
+ \hline
+ The tree is empty & Declare a judgment & A judgment \\
+ The focused goal has a candidate & Focus on a subgoal & An index \\
+ The focused goal has no candidate & Use an asset to prove the goal & A name
+ \end{tabular}
+
+ Here's what the actions do:
+
+ \begin{description}
+ \item[Declare] Place each pressuposition of the judgment as a
+ root in the goals tree, with no candidate.
+
+ \item[Focus] Add that subgoal's assumptions the assets table,
+ with a link to the subgoal. Focus on the subgoal.
+
+ \item[Use] Set the given name as the candidate for the focused
+ goal. If the name refers to an asset with assumptions, place those
+ assumptions as children of the current goal with no candidates. If
+ it does not, and it matches the focused goal, simply remove the
+ focused goal, remove assets introduced at that goal, and shift
+ focus to its parent. If instead it does not match, raise an error.
+ \end{description}
+
+ There's one thing missing from this description, which is
+ how to build subcontexts. Ideally, those would come from the
+ same process as the top-level context. And, actually, even the
+ top-level context can reasonably be expected to be packaged in
+ much the same way as the subcontexts. So, this suggests the
+ following approach, analogous to how we are handling goals:
+ build a context, then package it up into a subcontext of a new
+ goal. Repeat.
+
+ One choice: we have to either signal where we are \emph{starting}
+ a new subcontext (which drops us into the children of a
+ yet-to-be-defined judgment), or we can say, when \emph{closing}
+ it, where it starts (perhaps by refering to a label). The latter
+ is kinda clumsy and not very readable. So let's go for the first.
+
+ An alternative to the use-focus duo, and which would be terser,
+ would be to automatically focus on the first subgoal, when
+ applicable. An example of syntax for this second style could be
+ like this:
+
+ \begin{lstlisting}
+ #syntax suffix wff
+ #syntax infix :
+ #syntax suffix wft
+
+ { // start subcontext
+ [cv] x var
+ } [var-wff] x wff
+
+ {
+ [cc] c const // No pressups
+ } [cw] c wff;
+
+ [tc] type const // No pressup
+ [tt] type wft // Pressuposition: `type wff`
+ cw // Adds cc as subgoal
+ tc // Solves it, unifies `c` and `type`
+
+
+ {
+ [av] a var // No pressupositions
+ [at] a : type // Pressup `type wft`, `a wff`
+ tt // Solves first
+ var-wff // Adds cv
+ av // Solves it, unifies
+ } [type-wft] a wft
+ \end{lstlisting}
+
+ \subsection{Discussion}
+
+ The way we are approaching this is not the way its usually done
+ in logic, but rather in the narrow field of proofs assistants. In
+ the end, its the same thing: in logic, we describe these pristine
+ objects, regardless of how they could be built, and provide
+ validity conditions that distinguish them among the many others
+ syntactically correct, but invalid siblings.
+
+ In proof assistants, we describe \emph{programs} that run on
+ machines which \emph{build} such objects. A valid object, then, is
+ one that can be built by this machine using a particular program.
+
+ It's the same thing with grammars and automata.
+
+ The objects that we are describing are the contexts in the Logic
+ of Assumptions. They are a dependent list of assumptions, each
+ possibly using and refering to the previous ones, each carrying
+ with it the necessary proofs of its pressupositions. But,
+ of course, its easier to think about how one would go about
+ \emph{building} such a thing.
+
+\end{document}
diff --git a/writing/journal/2023-11-29-unification.tex b/writing/journal/2023-11-29-unification.tex
@@ -0,0 +1,65 @@
+\documentclass[../main.tex]{subfiles}
+
+\begin{document}
+
+ \section{2023-11-29 Unification in LoA proofs}
+
+ At a particular point during interaction with the LoA assistant,
+ when we finally apply to a goal an assumption without
+ subassumptions, the system will perform the simplification
+ procedure on the goal tree. That procedure involves recursively
+ (depth-first) checking that each applied assumption indeed matches
+ the goal at that level. That is, \emph{after} substitution. And that
+ is the snag. Substitution, at this point, is what ends up demanding
+ of us that we bake variable bindings onto terms; of course,
+ otherwise, we'd have no way of knowing which variables we \emph{can}
+ and which variables we \emph{cannot} replace.
+
+ Let's look at this example:
+
+ \begin{lstlisting}
+ {
+ [tp] t param
+ [xp] x param
+ [xv] x var
+ xp
+ [tt] t term
+ tp
+ } [lambda-term] lam(x, t) term
+ \end{lstlisting}
+
+ If we want to prove that \lstinline{lam(x, x) term}, we'd proceed as
+ follows:
+
+ \begin{lstlisting}
+ {
+ [yp] y param
+ [yv] y var
+ yp
+ } ! id-term lam(y, y) term
+ lambda-term // push `lam(y, t) term` as candidate
+ // First subgoal: `t param`
+ var-term // Use `y term`; subgoal: `y var`
+ yv // Substitution: `t := y`
+ // Second subgoal: `y param`
+ var-term
+ yv // Substitution: `y := y`
+ // Third subgoal: `y var`
+ yv
+ // Fourth subgoal: `y term`
+ var-term
+ yv
+ \end{lstlisting}
+
+ The variable is a parameter on the assumption as well. Otherwise,
+ we'd have no way of using other variables that are not the one
+ mentioned verbatim on the subcontext of the assumption. That is,
+ things that are not parameters work almost like punctuation.
+
+ The above proof, compacted, would read:
+
+ \begin{lstlisting}
+ { @ yp (param y) @ yv (var y) yp } ! id-term (term (lam y y)) lambda-term var-term yv var-term yv yv var-term yv
+ \end{lstlisting}
+
+\end{document}
diff --git a/writing/main.tex b/writing/main.tex
@@ -0,0 +1,149 @@
+\documentclass{article}
+
+\usepackage[english]{personal}
+
+\setmainfont{EB Garamond}
+% \setmonofont{}
+% \setsansfont{}
+\setmainlanguage{english}
+
+\title{A Logic of Assumptions}
+\author{Juan F. Meleiro}
+\date{2023}
+
+\begin{document}
+
+ \maketitle
+
+ A logical system is usually composed of a series of data. At least a type of signatures; and for each signature a type of judgments; and for each judgment a type of proofs; or alternativelly a notion of (in)compatibility between the judgments; etc.
+
+ But could we subsume all this concepts into a single one? Yes, I believe, and that would be the concept of \emph{assumption}. More specifically, of \emph{relative assumptions}. Let's get straight into it.
+
+ The system is composed of two layers. The first, purely combinatorial. It has two concepts, which define just the plain syntactical objects (grammar notwithstanding). Those are \definiendum{terms} and \definiendum{judgment forms}.
+
+ Then, the second layer, properlyl logical. It contains five interconected concepts, the most substantial of which is the \definiendum{assumption}, as we said. Assumptions are organized into \definiendum{contexts}, which relate to one another via \definiendum{translations}, which can be \definiendum{applied} to terms, and that is the basis of \definiendum{proofs}, which finally make assumptions well-formed.
+
+ So, schematically,
+
+ \begin{center}
+ \parbox{\textwidth}{
+ \framebox[0.5\textwidth]{Terms}
+ \framebox[0.5\textwidth]{Judgments}
+ }
+ \parbox{\textwidth}{
+ \framebox[0.2\textwidth]{Assumptions}
+ \framebox[0.2\textwidth]{Contexts}
+ \framebox[0.2\textwidth]{Translations}
+ \framebox[0.2\textwidth]{Application}
+ \framebox[0.2\textwidth]{Proofs}
+ }
+ \end{center}
+
+ \section{Definitions}
+
+ We start by supposing a fixed type for symbols \note{which must include three distinguished symbols called $\mathsf{symb}$, $\mathsf{var}$, and $\mathsf{judg}$}.
+
+ \begin{definition}[Terms]
+ \definiendum{Terms} are labelled trees of symbols. That is, a symbol called its \definiendum{head} plus a list of terms called its \definiendum{subterms}.
+ \end{definition}
+
+ \begin{definition}[Judgment forms]
+ \definiendum{Judgment forms} are a family of symbols associated with arities. Each judgment form has some \definiendum{pressupositions} which are other judgment forms using the same arguments.
+ \end{definition}
+
+ That's it for syntax.
+
+ Now for the logic.
+
+ \begin{definition}[Context]
+ A \definiendum{context} is either empty or a context (called its \definiendum{precontext}) and an assumption over it.
+ \end{definition}
+
+ \begin{definition}[Assumption]
+ An \definiendum{assumption} over a context is a judgment, a context (called its \definiendum{subcontext}), plus proofs for its pressupositions under the given context and the subcontext.
+ \end{definition}
+
+ \begin{definition}[Proof]
+ A \definiendum{proof} of a judgment in a collection of contexts is an assumption in one of them, plus a morphism from its subcontext into the collection.
+ \end{definition}
+
+ \begin{definition}[Morphism]
+ A morphism from a context (the \definiendum{domain}) into a collection of contexts (the \definiendum{codomain}) is
+ \begin{itemize}
+ \item If the domain is empty, nothing.
+ \item If the domain is a precontext and an assumption, a morphism from that precontext to the codomain plus a function taking a morphism from the assumptions subcontext to the codomain to a proof in the codomain of the translation of the assumption's judgment under the precontext morphism.
+ \end{itemize}
+ \end{definition}
+
+ \begin{definition}[Translation]
+ The translation of a judgment via a morphism is that same judgment form applied to the translated terms. A term translated via a morphism is the term associated with its head symbol with the translated subterms substituted into the variables.
+ \end{definition}
+
+ \section{Examples}
+
+ Let's build modus ponens. Our judgments are unary $\mathsf{true}$, unary $\mathsf{prop}$, plus the standard ones $\mathsf{symb}$ and $\mathsf{var}$. $\mathsf{true}$ judgments pressupose $\mathsf{prop}$ ones, and $\mathsf{prop}$ ones pressupose $\mathsf{var}$ ones (this means \emph{not} that all propositions are variables, but that to \emph{assume} something is a proposition, it must be known to be a variable).
+
+ \begin{lstlisting}[
+ mathescape=true,
+ literate={=>}{{$\Rightarrow$}{ }}{2}{:=}{{$\defeq$}}{1}{->}{{$\to$}{ }}{2},
+ basicstyle=\sffamily,
+ ]
+ var2prop {
+ var$_\alpha$ {} $\alpha$ var
+ triv
+ } $\alpha$ prop
+
+ fn-form {
+ var$_\alpha$ {} $\alpha$ var
+ triv
+ var$_\beta$ {} $\beta$ var
+ triv
+ prop$_\alpha$ {} $\alpha$ prop
+ prop$_\beta$ {} $\beta$ prop
+ } $\alpha$ -> $\beta$ prop
+
+ mp {
+ var$_\alpha$ {} $\alpha$ var
+ triv
+ var$_\beta$ {} $\beta$ var
+ triv
+ maj {} $\alpha$ -> $\beta$ true
+ fn-form
+ var$_\alpha$ => $\alpha$
+ var$_\beta$ => $\beta$
+ prop$_\alpha$ => var2prop
+ var$_\alpha$ => $\alpha$
+ prop$_\beta$ => var2prop
+ var$_\alpha$ => $\alpha$
+ min {} $\alpha$ true
+ var2prop
+ var$_\alpha$ => $\alpha$
+ } $\beta$ true
+ var2prop
+ var$_\alpha$ => @var$_\beta$
+
+ dt {
+ var$_\beta$ {} $\beta$ var
+ triv
+ var$_\alpha$ {} $\alpha$ var
+ triv
+ prop$_\beta$ {} $\beta$ prop
+ var$_\beta$
+ prop$_\alpha$ {} $\alpha$ prop
+ var$_\alpha$
+ hyp {
+ cond {} $\alpha$ true
+ prop$_\alpha$
+ } $\beta$ true
+ prop$_\beta$
+ } $\alpha$ -> $\beta$ true
+ fn-form
+ var$_\alpha$ => @var$_\alpha$
+ var$_\beta$ => @var$_\beta$
+ prop$_\alpha$ => var2prop
+ var$_\alpha$ => @var$_\alpha$
+ prop$_\beta$ => var2prop
+ var$_\alpha$ => @var$_\beta$
+ \end{lstlisting}
+
+\end{document}
diff --git a/writing/manage b/writing/manage
@@ -0,0 +1,12 @@
+#!/usr/bin/fish
+switch $argv[1]
+ case monitor
+ fd --extension tex --extension bib | entr redo
+ case workspace
+ rubber -m xelatex main.tex
+ r main.pdf >/dev/null 2>&1 &
+ emacsclient -c -n main.tex &
+ ./manage monitor
+ case clean
+ rm -f *.{aux,log,out,bcf,run.xml,bbl,blg,nav,rubbercache,snm,toc,vrb}
+end
diff --git a/writing/notes/2jd6ltd1j0k0.md b/writing/notes/2jd6ltd1j0k0.md
@@ -0,0 +1 @@
+Declaring a judgement means from then on, when you have to prove it, you can use its subjudgements, and you must prove its subjudgements in order to use it.
diff --git a/writing/simple-case.lisp b/writing/simple-case.lisp
@@ -0,0 +1,35 @@
+(assums (a x) (var x))
+(assums (b x) (var x))
+(assums (c x) (var x))
+
+;; CTX := (NAME [ASSUM])
+;; ASSUM := (NAME CTX EXPR [PROOF])
+;; PROOF := (NAME => (NAME [PROOF]))
+
+(careful
+
+ (a2b (vx () (var x) ()
+ aa () (a x) (vx))
+ (b x))
+
+ (b2c (vx () (var x) ()
+ ab () (b x) (vx))
+ (c x)))
+
+(hasty
+
+ (a2c (aa () (a x))
+ (c x)))
+
+(implement hasty careful
+ (a2c b2c
+ (ab a2b
+ (a2c.aa))))
+
+(prove hasty.a2c ; goals: [a2c]
+ careful.b2c ; goals: [careful.b2c.vx, careful.b2c.ab]
+ triv ; goals: [careful.b2c.ab]
+ careful.a2b ; goals: [careful.a2b.vx, careful.a2b.aa]
+ triv ; goals: [careful.a2b.aa]
+ hasty.a2c.aa ; goals: []
+ )
