Skip to content

Commit c8a5980

Browse files
ratmiceratmice
committed
chowder parser experiment 1.
1 parent ba4d03f commit c8a5980

File tree

9 files changed

+429
-118
lines changed

9 files changed

+429
-118
lines changed

‎docs/Makefile

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
.PHONY: clean
2+
3+
inference_rules.pdf: inference_rules.tex
4+
xelatex inference_rules.tex
5+
6+
clean:
7+
rm -f *.aux *.pdf *.fdb_latexmk *.log *.fls

‎docs/chowder.ebnf

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
Name ::= [a-zA-Z][a-zA-Z0-9]*
2+
Bindings ::= (Binding ";") Binding?
3+
Binding ::= Name (":" Prop)? "≔" Stmt
4+
Stmt ::= Stmt "‣" Thus | Thus
5+
Thus ::= Thus "∴" PropOpt | Thus "." PropOpt | PropOpt
6+
PropOpt ::=
7+
()
8+
| Prop
9+
10+
Prop ::= "¬" BinaryProp | BinaryProp
11+
BinaryProp ::=
12+
BinaryProp "∧" Atom
13+
| BinaryProp "∨" Atom
14+
| BinaryProp "→" Atom
15+
| BinaryProp "↔" Atom
16+
| BinaryProp "∧" "¬" Atom
17+
| BinaryProp "∨" "¬" Atom
18+
| BinaryProp "→" "¬" Atom
19+
| BinaryProp "↔" "¬" Atom
20+
| Atom
21+
22+
Atom ::= "T" | "(" Prop ")" | Name

‎docs/inference_rules.tex

Lines changed: 247 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,247 @@
1+
\documentclass{article}
2+
\usepackage{bussproofs}
3+
\usepackage{amsfonts,amsmath,amssymb,amsthm}
4+
\usepackage{amsmath}
5+
\usepackage{marvosym}
6+
\usepackage{unicode-math}
7+
\usepackage[margin=0.5in]{geometry}
8+
\usepackage{newunicodechar}
9+
\usepackage{fancyvrb}
10+
\AtBeginDocument{\setmainfont{XITS-Regular.otf}}
11+
\AtBeginDocument{\setmathfont{XITSMath-Regular.otf}}
12+
\AtBeginDocument{\newfontfamily{\mathfont}{FreeMono.otf}}
13+
14+
15+
\AtBeginDocument{\newunicodechar{→} {\mathfont{→}}}
16+
\AtBeginDocument{\newunicodechar{∀} {\ensuremath{\forall}}}
17+
\AtBeginDocument{\newunicodechar{∃} {\ensuremath{\exists}}}
18+
\AtBeginDocument{\newunicodechar{‣} {\mathfont{‣}}}
19+
\AtBeginDocument{\newunicodechar{∴} {\mathfont{∴}}}
20+
\AtBeginDocument{\newunicodechar{≔} {\mathfont{≔}}}
21+
\AtBeginDocument{\newunicodechar{⋮} {\mathfont{⋮}}}
22+
\AtBeginDocument{\newunicodechar{∧} {\mathfont{∧}}}
23+
\AtBeginDocument{\newunicodechar{∨} {\mathfont{∨}}}
24+
\AtBeginDocument{\newunicodechar{⚡} {\mbox{\Lightning}}}
25+
26+
\title{"Chowder" proof checking inference rules augmented with proposed syntax}
27+
\author{matt rice}
28+
29+
\newenvironment{bprooftree0}
30+
{\leavevmode\hbox\bgroup}
31+
{\DisplayProof\egroup}
32+
\newenvironment{bprooftree}
33+
{\noindent\hbox\bgroup}
34+
{\DisplayProof\egroup}
35+
36+
\newcommand{\charge}[2]{%
37+
\LeftLabel{$\smalltriangleright$}
38+
\RightLabel{$^+\text{\Lightning}\alpha$}
39+
\AxiomC{}%
40+
\UnaryInfC{#1}%
41+
\noLine%
42+
\UnaryInfC{$\vdots$}%
43+
\noLine%
44+
\UnaryInfC{#2.}}%
45+
46+
\newcommand{\discharge}[1]{%
47+
\LeftLabel{$^-\text{\Lightning}\alpha$}%
48+
\RightLabel{#1}%
49+
}%
50+
51+
\newcommand{\thus}[1]{%
52+
$\therefore$ #1
53+
}
54+
\newcommand{\biimpl}{\leftrightarrow}
55+
\newcommand{\hsep}{\vspace{1em}\par}
56+
\newcommand{\vsep}{\hspace{0.5em}%
57+
%\vrule%
58+
\hspace{0.5em}}
59+
60+
\begin{document}
61+
62+
\maketitle
63+
64+
\section{Inference rules}
65+
Natural deduction rules augmented with chowder syntax
66+
\description
67+
\item{$\smalltriangleright$} acts as n-ary case analysis.
68+
\item{$\therefore$} acts like the natural deduction mid-line in syntax.
69+
\par
70+
\vspace{1em}
71+
Conjunction:
72+
\begin{bprooftree}
73+
\AxiomC{A}
74+
\AxiomC{B}
75+
\RightLabel{\thus{$\wedge$I}}
76+
\BinaryInfC{A $\wedge$ B}
77+
\end{bprooftree}
78+
\begin{bprooftree}
79+
\AxiomC{A $\wedge$ B}
80+
\RightLabel{\thus{$\wedge E_L$}}
81+
\UnaryInfC{A}
82+
\end{bprooftree}
83+
\begin{bprooftree}
84+
\AxiomC{A $\wedge$ B}
85+
\RightLabel{\thus{$\wedge E_R$}}
86+
\UnaryInfC{B}
87+
\end{bprooftree}
88+
\hsep
89+
Disjunction:
90+
\begin{bprooftree}
91+
\AxiomC{A}
92+
\LeftLabel{}
93+
\RightLabel{\thus{$\vee I_L$}}
94+
\UnaryInfC{A $\vee$ B}
95+
\end{bprooftree}
96+
\begin{bprooftree}
97+
\AxiomC{B}
98+
\RightLabel{\thus{$\vee I_R$}}
99+
\UnaryInfC{ A $\vee$ B}
100+
\end{bprooftree}
101+
\begin{bprooftree}
102+
\AxiomC{A $\vee$ B}
103+
\charge{A}{C}
104+
\charge{B}{C}
105+
\discharge{\thus{$\vee E$}}
106+
\TrinaryInfC{C}
107+
\end{bprooftree}
108+
109+
\hsep
110+
Implication:
111+
\begin{bprooftree}
112+
\charge{A}{B}
113+
\discharge{\thus{$\to$I}}
114+
\UnaryInfC{A $\to$ B}
115+
\end{bprooftree}
116+
\begin{bprooftree}
117+
\AxiomC{$\neg$A}
118+
\AxiomC{A}
119+
\RightLabel{\thus{$\neg$E}}
120+
\BinaryInfC{$\bot$}
121+
\end{bprooftree}
122+
Negation:
123+
\begin{bprooftree}
124+
\charge{A}{$\bot$}
125+
\discharge{\thus{$\neg$I}}
126+
\UnaryInfC{$\neg$A}
127+
\end{bprooftree}
128+
\begin{bprooftree}
129+
\AxiomC{A $\to$ B}
130+
\AxiomC{A}
131+
\RightLabel{\thus{$\to$E}}
132+
\BinaryInfC{B}
133+
\end{bprooftree}
134+
135+
\hsep
136+
137+
Top:
138+
\begin{bprooftree}
139+
\AxiomC{}
140+
\RightLabel{$\top$I}
141+
\UnaryInfC{$\top$}
142+
\end{bprooftree}
143+
144+
\hsep
145+
146+
Bot:
147+
\begin{bprooftree}
148+
\AxiomC{$\bot$}
149+
\RightLabel{\thus{$\bot$E}}
150+
\UnaryInfC{A}
151+
\end{bprooftree}
152+
\hsep
153+
154+
Bi-implication:
155+
156+
\begin{bprooftree}
157+
\charge{A}{B}
158+
\charge{B}{A}
159+
\discharge{\thus{$\leftrightarrow$I}}
160+
\BinaryInfC{A $\biimpl$ B}
161+
\end{bprooftree}
162+
\begin{bprooftree}
163+
\AxiomC{A $\biimpl$ B}
164+
\AxiomC{A}
165+
\RightLabel{\thus{$\biimpl{E_L}$}}
166+
\BinaryInfC{B}
167+
\end{bprooftree}
168+
\begin{bprooftree}
169+
\AxiomC{A $\biimpl$ B}
170+
\AxiomC{B}
171+
\RightLabel{\thus{$\biimpl{E_R}$}}
172+
\BinaryInfC{A}
173+
\end{bprooftree}
174+
\section{EBNF}
175+
\begin{Verbatim}
176+
Name ::= [a-zA-Z][a-zA-Z0-9]*
177+
Bindings ::= (Binding ";") Binding?
178+
Binding ::= Name (":" Prop)? "≔" Stmt
179+
Stmt ::= Stmt "‣" Thus | Thus
180+
Thus ::= Thus "∴" PropOpt | Thus "." PropOpt | PropOpt
181+
PropOpt ::=
182+
()
183+
| Prop
184+
185+
Prop ::= "¬" BinaryProp | BinaryProp
186+
BinaryProp ::=
187+
BinaryProp "∧" Atom
188+
| BinaryProp "∨" Atom
189+
| BinaryProp "→" Atom
190+
| BinaryProp "↔" Atom
191+
| BinaryProp "∧" "¬" Atom
192+
| BinaryProp "∨" "¬" Atom
193+
| BinaryProp "→" "¬" Atom
194+
| BinaryProp "↔" "¬" Atom
195+
| Atom
196+
Atom ::= "T" | "(" Prop ")" | Name
197+
\end{Verbatim}
198+
199+
\section{Some unchecked proofs that parse.}
200+
201+
\begin{Verbatim}
202+
ab_or_cd: (A ∧ B) ∨ (C ∧ D) → B ∨ D
203+
≔ ‣ (A ∧ B) ∨ (C ∧ D) ;; +⚡1
204+
‣ A ∧ B ;; +⚡2
205+
∴ B ;; ∴ ∧E R
206+
∴ B ∨ D. ;; ∴ ∨I L
207+
‣ C ∧ D ;; +⚡2
208+
∴ D ;; ∴ ∧E R
209+
∴ B ∨ D. ;; ∴ ∨I R
210+
∴ B ∨ D. ;; -⚡2 ∴ ∨E
211+
∴ (A ∧ B) ∨ (C ∧ D) → B ∨ D. ;; -⚡1 ∴ →I
212+
;
213+
\end{Verbatim}
214+
215+
216+
\begin{Verbatim}
217+
iff_and_or: (A ∧ B) ∨ (C ∧ D) ↔ (B ∧ A) ∨ (D ∧ C)
218+
≔ ‣‣(A ∧ B) ∨ (C ∧ D) ;; +⚡1, +⚡2
219+
‣ A ∧ B ;; +⚡3
220+
∴ B ;; ∴ ∧E R
221+
∴ A ;; ∴ ∧E L
222+
∴ B ∧ A ;; ∴ ∧I
223+
∴ (B ∧ A) ∨ (D ∧ C). ;; ∴ ∨I L
224+
‣ C ∧ D ;; +⚡3
225+
∴ D ;; ∴ ∧E R
226+
∴ C ;; ∴ ∧E L
227+
∴ D ∧ C ;; ∴ ∧I
228+
∴ (B ∧ A) ∨ (D ∧ C). ;; ∴ ∨I L
229+
∴ (B ∧ A) ∨ (D ∧ C). ;; -3 ∴ ∨E
230+
∴ (A ∧ B) ∨ (C ∧ D) → (B ∧ A) ∨ (D ∧ C). ;; -2 ∴ →I
231+
‣‣ (B ∧ A) ∨ (D ∧ C) ;; +⚡1, +⚡2
232+
‣ B ∧ A ;; +⚡3
233+
∴ B ∧ A ∴ A ;; ∴ ∧E R
234+
∴ B ∧ A ∴ B ;; ??, ∴ ∧E L
235+
∴ A ∧ B ;; ∴ ∧I
236+
∴ (A ∧ B) ∨ (C ∧ D). ;; ∴ ∨I L
237+
‣ D ∧ C ;; +⚡3
238+
∴ C ;; ∴ ∧E R
239+
∴ D ;; ??, ∴ ∧E L
240+
∴ C ∧ D ;; ∴ ∧I
241+
∴ (A ∧ B) ∨ (C ∧ D). ;; ∴ ∨I R
242+
∴ (A ∧ B) ∨ (C ∧ D). ;; -⚡3 ∴ ∨E
243+
∴ (B ∧ A) ∨ (D ∧ C) → (A ∧ B) ∨ (C ∧ D). ;; -⚡2 ∴ →I
244+
∴ (A ∧ B) ∨ (C ∧ D) ↔ (B ∧ A) ∨ (D ∧ C). ;; -⚡1 ∴ ↔I
245+
;
246+
\end{Verbatim}
247+
\end{document}

‎src/ast.rs

Lines changed: 0 additions & 74 deletions
This file was deleted.

0 commit comments

Comments
 (0)