Skip to content
Snippets Groups Projects
Commit 7ac960ff authored by Ioanna M. Dimitriou H.'s avatar Ioanna M. Dimitriou H. 💬
Browse files

All tests ok, updated README.

parent 6acb36fe
Branches
No related tags found
No related merge requests found
......@@ -4,28 +4,35 @@ This is the early stage of a program which creates diagrams with the relationshi
**Consequences of the Axiom of Choice Project**
by Prof. Paul Howard and Prof. Jean E. Rubin. I thank Paul Howard for providing me with the implication matrix (book1), a tex document with the form statements in LaTeX form, and permision to use these files, which can be found in the folder "Howard-Rubin-data".
A quick overview is given below. A paper with a full description and explanation of the code will appear after I upload the diagram drawing part of this program. A big *thank you* to my Common-Lisp teacher, Max Rottenkolber, for coming up with the graph-structure for this program, for naming Jeffrey, and for his lessons and advice.
A quick overview is given below. A paper with a full description and explanation of the code will appear after I upload the diagram drawing part of this program. A big *thank you* to my teammate Max Rottenkolber over at [interstellar ventures](http://inters.co).
## Installation
Install this package using quicklisp ([installation instructions](https://www.quicklisp.org/beta/#installation)) and git ([installation instructions](https://git-scm.com/book/en/v2/Getting-Started-Installing-Git)) as follows:
* Create a folder called `jeffrey` in `quicklisp/local-projects/`,
* Navigate to this folder in a terminal and type `git init` and `git clone git@github.com:ioannad/jeffrey.git`. Alternatively otherwise download the contents of this repository to this folder.
To produce a diagram, open an SBCL Common Lisp REPL (I haven't tested it yet in other Common-Lisp implementations, please let me know if it works!). Then type in `(ql:quickload "jeffrey")`. Then choose a package you'd like to use, for example to run all tests and read the report type in `(in-package :jeffrey.test)` and then type in `(test-all)`.
## Description
This program requires package "mpc" and "split-sequence". In the to-do list is to change mpc to maxpc, the new version of mpc.
**jeffrey.asd** contains the (defsystem ...) command that creates "jeffrey" as a system of packages. The files that comprise jeffrey's packages, their exported functions, and their dependencies are listed in **packages.lisp**.
**graph.lisp** contains the graph structure where the information is stored (the types), and the related functions, which are the basic language of the system. There are two types, one type *node*, which is a name of type natural number, a list of edges of type edge described below, a list of parents of type node, a LaTeX statement of type string, references of type string, and a placeholder for attributes. The other type is *edge*, which is a destination of type node, a relation (T or NIL), which corresponds to positive and negative implication arrow respectively, and a placeholder for attributes. The nodes are to be stored in the exported hash-table *graph*.
**graph.lisp** contains the graph structure where the information is stored (the types), and the related functions, which are the basic language of the system. There are two types, one type `node`, which is a name of type natural number, a list of edges of type edge described below, a list of parents of type node, a LaTeX statement of type string, references of type string, and a placeholder for attributes. The other type is `edge`, which is a destination of type node, a relation (T or NIL), which corresponds to positive and negative implication arrow respectively, and a placeholder for attributes. The nodes are to be stored in the exported hash-table `\*graph\*`.
**parse.lisp** contains parsing functions for reading in node (form) information, and for reading book1, the original matrix with all the implication codes. Form information, i.e., name, LaTeX-statement, and references are parsed in a machete-style chopping of the TeX-file Howard-Rubin-data/FORMSNUM.TEX. Implication information is parsed simply, because book1 is a simple integer matrix whose lines terminate with -1.
**parse.lisp** contains parsing functions for reading in node (form) information, and for reading `book1`, the original matrix with all the implication codes. Form information, i.e., name, LaTeX-statement, and references are parsed in a machete-style chopping of the TeX-file `Howard-Rubin-data/FORMSNUM.TEX`. Implication information is parsed simply, because book1 is a simple integer matrix whose lines terminate with -1.
**read.lisp** contains the functions that read input, and it can be run in its whole with (read-all-data). This function will
first store the form data from FORMSNUM.TEX as nodes in \*graph\*, then add edges and parents to these nodes, following only the direct information from book1. That is, if book1 has code 1 in position (i,j), then it will add an edge to the node with name i (node i) with destination node j and relation T, and it will add node i to the set of parents of node j. If book1 has code 3 in position (i,j), then it will only add an edge to node i with destination node j and relation NIL. All other codes should be derivable from this information, using the predicates in the next module.
**read.lisp** contains the functions that read input, and it can be run in its whole with `(read-all-data)`. This function will first store the form data from `FORMSNUM.TEX` as nodes in `\*graph\*`, then add edges and parents to these nodes, following only the direct information from `book1`. That is, if book1 has code 1 in position (i,j), then it will add an edge to the node with name i (node i) with destination node j and relation T, and it will add node i to the set of parents of node j. If book1 has code 3 in position (i,j), then it will only add an edge to node i with destination node j and relation NIL. All other codes should be derivable from this information, using the predicates in the next module.
**predicates.lisp** enables the program to ask whether or not a node (form) implies another. The function implies-p only answers positive implication questions, and implies-not-p only answers negative implication questions. In particular, (implies-p A B) asks whether A is an ancestor of B and (implies-not-p B A) asks whether there is an ancestor B' of B and a descendant A' of A, such that the *node* B' has an edge with destination A' and relation NIL. Why is the predicate "implies-p" defined like this is clear. For (implies-not-p B A), assume that there is an ancestor B-anc of B and a descendant A-desc of A, such that B-anc does not imply A-desc (the meaning of a NIL-edge from B-anc to A-desc). Then (implies-not-p B A) must be T, i.e., B does not imply A, because otherwise we have the implication chain:
**predicates.lisp** enables the program to ask whether or not a node (form) implies another. The function implies-p only answers positive implication questions, and implies-not-p only answers negative implication questions. In particular, `(implies-p A B)` asks whether A is an ancestor of B and `(implies-not-p B A)` asks whether there is an ancestor B' of B and a descendant A' of A, such that the node B' has an edge with destination A' and relation NIL. Why is the predicate "implies-p" defined like this is clear. For `(implies-not-p B A)`, assume that there is an ancestor B-anc of B and a descendant A-desc of A, such that B-anc does not imply A-desc (the meaning of a NIL-edge from B-anc to A-desc). Then `(implies-not-p B A)` must be T, i.e., B does not imply A, because otherwise we have the implication chain:
B-anc implies B implies A implies A-desc,
therefore B-anc implies A-desc, contradiction to the NIL-edge from B-desc to A-desc.
**test.lisp** contains test data and testing functions, which should be run after every and any change in the above files.
At this moment, only (test-predicates), (test-read), and (test-add-edge) pass, and checking the matrix against book1 has by now resulted in the temporary removal of two forms (374 and 423) which turn out to be equivalent and thus create a loop. This test is not finished yet.
Run all tests while `(in-package :jeffrey-test)` with the command `(test-all)`, which prints a report to your REPL.
**/sneak-preview/** contains diagrams with sets of forms that make sense, e.g., between forms about alephs and their properties, as well as diagrams with random sets of forms. A boldfaced arrow from A to B means that the implication is non-reversible, i.e., there exists a model of ZF set theory in which B holds and A doesn't. *Just imagine the endless possibilities for random research projects, theses, and papers, filling or boldfacing those arrows! :)* The full-diagram.pdf is also included, only for standard "number names" (not full statements). Its size is 3,63m x 78 cm.
**/sneak-preview/** contains diagrams with sets of forms that make sense, e.g., between forms about alephs and their properties, as well as diagrams with random sets of forms. A boldfaced arrow from A to B means that the implication is non-reversible, i.e., there exists a model of ZF set theory in which B holds and A doesn't. *Just imagine the endless possibilities for random research projects, theses, and papers, filling or boldfacing those arrows! :)* The `full-diagram.pdf` is also included, only for standard "number names" (not full statements). Its size is 3,63m x 78 cm.
**complexity issues**
I haven't really tried to optimize this algorithm yet (from the graph structure to the diagram), apart from the addition of the *jeff-matrix* that remembers the answers of the predicates. This could be made even faster, but it's not necessary now.
......
......
......@@ -31,6 +31,8 @@
:mpc :mpc.characters :mpc.numerals)
(:export :*local-directory*
:*bad-forms* ;; export for testing only
:*book-file* ;; export for testing only
:read-book1 ;; export for testing only
:matrix-to-graph ;; export for testing only
:graph-to-matrix
:add-top-bottom ;; export for testing only
......@@ -71,7 +73,7 @@
:jeffrey.read
:jeffrey.draw)
(:export :main)
(:documentation "<PACKAGE UNDER PRODUCTION> Install this package in using quicklisp (installation instructions for quicklisp can be found in https:////www.quicklisp.org//beta//#installation) and git (https:////git-scm.com//book//en//v2//Getting-Started-Installing-Git) as follows:
(:documentation "<PACKAGE UNDER PRODUCTION> Install this package using quicklisp (installation instructions for quicklisp can be found in https:////www.quicklisp.org//beta//#installation) and git (https:////git-scm.com//book//en//v2//Getting-Started-Installing-Git) as follows:
* Create a folder called `jeffrey` in `quicklisp//local-projects//`,
* Navigate to this folder in a terminal and type `git init` and `git clone git@github.com:ioannad//jeffrey.git`. Alternatively otherwise download the contents of this repository to this folder.
......
......
......@@ -119,19 +119,40 @@
i j #1#)))))
(format t "Passed test-matrix-equivalency.~%"))
(defun compare-equivalents? (stream name-1 name-2 book1-list)
(format stream "Comparison of codes for node ~a and node ~a, only printing the places where the codes are *not* equal:~%~%~%"
name-1 name-2)
(loop for i from 0 to 430
when (or (not (equal #1=(nth name-1 (nth i book1-list))
#2=(nth name-2 (nth i book1-list))))
(not (equal #3=(nth i (nth name-1 book1-list))
#4=(nth i (nth name-2 book1-list)))))
do (format t "(~a;~a) implies ~a = (~a;~a) respectively, and~% ~a implies (~a;~a) = (~a;~a) respectively.~%~%"
name-1 name-2 i
#1# #2#
i name-1 name-2
#3# #4#)))
(defun checkout-423-374 ()
(compare-equivalents? t 423 374 (read-book *book1-file*)))
(defun test-all ()
;; test data
(format t "Setting up test...~%")
(setup-test)
(format t "Testing add-edge...~%")
(format t "~%Testing add-edge...~%")
(test-add-edge)
(format t "Testing predicates with the test-matrix...~%")
(format t "~%Testing predicates with the test-matrix...~%")
(test-predicates)
(format t "Testing the reading module...~%")
(format t "~%Testing the reading module...~%")
(test-read)
;; book1
(format t "Testing equivalence of the filled out *jeff-matrix* with book1...~%")
(format t "~%Testing equivalence of the filled out *jeff-matrix* with book1...~%")
(let ((book1-matrix (read-all-data)))
(setup-jeff-matrix *graph*)
(fill-missing-positions-using-predicates *graph*)
(test-matrix-equivalency *jeff-matrix* book1-matrix)))
(test-matrix-equivalency *jeff-matrix* book1-matrix))
(format t "~%Still to do, take care of the equivalency between 374 and 423. Checking book1 for the codes in row 423 vs row 374, and column 423 vs column 374 gives the following places where these are not equal:~%")
(checkout-423-374))
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment