Commit 195c96f4 authored by François Thiré's avatar François Thiré

A first draft

parents
*.aux
*.glo
*.idx
*.log
*.toc
*.ist
*.acn
*.acr
*.alg
*.bbl
*.blg
*.dvi
*.glg
*.gls
*.ilg
*.ind
*.lof
*.lot
*.maf
*.mtc
*.mtc1
*.out
*.synctex.gz
*~
\#*\#
*.elc
.\#*
File added
\documentclass{article}
\input{packages.tex}
\input{macros.tex}
\author{François Thiré}
\date{\today}
\title{An abstract formalisation of lambda-pi modulo theory}
\begin{document}
\begin{figure}
\centering
\begin{tabular}{lccl}
\textbf{Variables} & \(x,y,z,\dots\) & & \\
\textbf{Sorts} & \(s\) & \(\defn\) & \(\ttype{} ~|~ \tkind\) \\
\textbf{Terms} & \(A,B,t,u\) & \(\defn\) & \(x~|~s~|~\tpi{x}{A}{B} ~|~\tabs{x}{A}{u} ~|~ \tapp{t}{u} \)\\
\textbf{Context} & \(\Gamma\) & \(\defn\) & \(\emptyset~|~\Gamma, x:A~|~\Gamma, \mathcal{R}\)\\
\textbf{Typing Judgment} & & & \(\Gamma \vdash t : A\)\\
\textbf{Typing context well-formed} & & & \(\vdash \wf{\Gamma}\) \\
\textbf{Relation well-formed} & & & \(\Gamma \vdash \wf{\mathcal{R}}\) \\
\end{tabular}
\caption{\lfmt{}}
\label{fig:sttsyntax}
\end{figure}
\begin{definition}
Let \(\mathcal{X}\) be a countable set of variables.
\end{definition}
\begin{definition}
We denote \(\mathcal{T}_{\mathcal{X}}\) the free algebra over the terms with variables in \(\mathcal{X}\).
\end{definition}
\begin{definition}
We define \(\mathfrak{R}_{\mathcal{X}}\) the set of pairs of terms:
\[\mathfrak{R}_{\mathcal{X}} \defn \{(t,u) \mid t,u \in \mathcal{T}_{\mathcal{X}}\} \]
\end{definition}
\begin{definition}
We denote \(Dom(\Gamma)\) the domain of \(\Gamma\) defines as:
\begin{align*}
Dom(\emptyset) &\defn \emptyset \\
Dom(\Gamma , x : A) &\defn Dom(\Gamma) \cup \{x\}
\end{align*}
\end{definition}
\begin{definition}
We define \(\conv_{\beta\Gamma}\) as the reflexive and transitive closure of \(\beta\) and \(\{\mathcal{R} \mid \mathcal{R} \in \Gamma\}\).
\end{definition}
\begin{rules}{typing}{Typing rules}
\inferrule{ }
{\wf{\emptyset}}
\and
\inferrule{
\wf{\Gamma}
\\
{\Gamma \vdash A : \ttype}
}
{\wf{\Gamma, x:A}}
\and
\inferrule{
\wf{\Gamma}
\\
{\mathcal{R} \in \mathfrak{R}_{Dom(\Gamma)}}
\\
{\Gamma \vdash \wf{\mathcal{R}}}
}
{\wf{\Gamma, \mathcal{R}}}
\and
\inferrule{
TODO
}
{\Gamma \vdash \wf{\mathcal{R}}}
\and
\inferrule{
\wf{\Gamma}
\\
x : A \in \Gamma
}
{\Gamma \vdash x : A}
\and
\inferrule{
}
{\Gamma \vdash \ttype : \tkind}
\and
\inferrule{
\Gamma \vdash A : \ttype
\\
\Gamma, x : A \vdash B : s
}
{\Gamma \vdash \tpi{x}{A}{B} : s}
\and
\inferrule{
\Gamma \vdash A : \ttype
\\
\Gamma, x : A \vdash B : s
\\
\Gamma, x : A \vdash t : B
}
{\Gamma \vdash \tabs{x}{A}{t} : \tpi{x}{A}{B}}
\and
\inferrule{
\Gamma \vdash t : \tpi{x}{A}{B}
\\
\Gamma \vdash u : A
}
{\Gamma \vdash t~u : \subst{B}{x}{u}}
\and
\inferrule{
\Gamma \vdash A : s
\\
A \conv_{\beta\Gamma} B
\\
\Gamma \vdash t : A
}
{\Gamma \vdash t: B}
\end{rules}
\end{document}
\ No newline at end of file
\newtheorem{definition}{Definition}
\newcommand{\lfmt}{\ensuremath{\lambda\Pi\text{-modulo theory}}}
\newcommand{\defn}{\ensuremath{:=}}
\newcommand{\tabs}[3]{\ensuremath{\lambda{#1}~:~{#2}.~{#3}}}
\newcommand{\tapp}[2]{\ensuremath{{#1}~{#2}}}
\newcommand{\tpi}[3]{\ensuremath{\Pi{#1}~:~{#2}.~{#3}}}
\newcommand{\ttype}{\ensuremath{\mathbf{Type}}}
\newcommand{\tkind}{\ensuremath{\mathbf{Kind}}}
\newcommand{\conv}{\ensuremath{\equiv}}
\newcommand{\wf}[1]{\ensuremath{{#1}~\mathbf{wf}}}
\newcommand{\subst}[3]{\ensuremath{#1[#2 \leftarrow #3]}}
\newenvironment{rules}[2]
{
\def\tmpvariable{#1}
\def\tmpvariabled{#2}
\begin{figure}
\begin{mdframed}
\begin{center}
\begin{mathpar}
}
{
\end{mathpar}
\end{center}
\renewcommand{\figurename}{Figure}
\caption{\tmpvariable}
\label{\tmpvariabled}
\end{mdframed}
\end{figure}
}
\ No newline at end of file
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{mathpartir}
\usepackage{mdframed}
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment