Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-devel
Commits
cb1f24a06749
Commit
d4be70b1
authored
Feb 24, 2021
by
Lawrence Paulson
Browse files
Formal_Puiseux_Series website
parent
74a42283f683
Changes
7
Expand all
Hide whitespace changes
Inline
Side-by-side
metadata/metadata
View file @
cb1f24a0
...
...
@@ -9676,6 +9676,23 @@ abstract =
p<sub><em>i</em></sub> for
i>k.</p>
[Formal_Puiseux_Series]
title = Formal Puiseux Series
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
topic = Mathematics/Algebra
date = 2021-02-17
notify = eberlm@in.tum.de
abstract =
<p>Formal Puiseux series are generalisations of formal power
series and formal Laurent series that also allow for fractional
exponents. They have the following general form: \[\sum_{i=N}^\infty
a_{i/d} X^{i/d}\] where <em>N</em> is an integer and
<em>d</em> is a positive integer.</p> <p>This
entry defines these series including their basic algebraic properties.
Furthermore, it proves the Newton–Puiseux Theorem, namely that the
Puiseux series over an algebraically closed field of characteristic 0
are also algebraically closed.</p>
[Gaussian_Integers]
title = Gaussian Integers
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
...
...
@@ -10232,8 +10249,8 @@ author = Jakub Kądziołka <mailto:kuba@kadziolka.net>
topic = Logic/General logic/Logics of knowledge and belief
date = 2021-01-30
notify = kuba@kadziolka.net
abstract =
In a <a href="https://xkcd.com/blue_eyes.html">puzzle published by
abstract =
In a <a href="https://xkcd.com/blue_eyes.html">puzzle published by
Randall Munroe</a>, perfect logicians forbidden
from communicating are stranded on an island, and may only leave once
they have figured out their own eye color. We present a method of
...
...
web/entries/Formal_Puiseux_Series.html
0 → 100644
View file @
cb1f24a0
<!DOCTYPE html>
<html
lang=
"en"
>
<head>
<meta
charset=
"utf-8"
>
<title>
Formal Puiseux Series - Archive of Formal Proofs
</title>
<link
rel=
"stylesheet"
type=
"text/css"
href=
"../front.css"
>
<link
rel=
"icon"
href=
"../images/favicon.ico"
type=
"image/icon"
>
<link
rel=
"alternate"
type=
"application/rss+xml"
title=
"RSS"
href=
"../rss.xml"
>
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax
=
{
tex
:
{
inlineMath
:
[[
'
$
'
,
'
$
'
],
[
'
\\
(
'
,
'
\\
)
'
]]
},
processEscapes
:
true
,
svg
:
{
fontCache
:
'
global
'
}
};
</script>
<script
id=
"MathJax-script"
async
src=
"../components/mathjax/es5/tex-mml-chtml.js"
></script>
</head>
<body
class=
"mathjax_ignore"
>
<table
width=
"100%"
>
<tbody>
<tr>
<!-- Navigation -->
<td
width=
"20%"
align=
"center"
valign=
"top"
>
<p>
</p>
<a
href=
"https://www.isa-afp.org/"
>
<img
src=
"../images/isabelle.png"
width=
"100"
height=
"88"
border=
0
>
</a>
<p>
</p>
<p>
</p>
<table
class=
"nav"
width=
"80%"
>
<tr>
<td
class=
"nav"
width=
"100%"
><a
href=
"../index.html"
>
Home
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../about.html"
>
About
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../submitting.html"
>
Submission
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../updating.html"
>
Updating Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../using.html"
>
Using Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../search.html"
>
Search
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../statistics.html"
>
Statistics
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../topics.html"
>
Index
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../download.html"
>
Download
</a></td>
</tr>
</table>
<p>
</p>
<p>
</p>
</td>
<!-- Content -->
<td
width=
"80%"
valign=
"top"
>
<div
align=
"center"
>
<p>
</p>
<h1>
<font
class=
"first"
>
F
</font>
ormal
<font
class=
"first"
>
P
</font>
uiseux
<font
class=
"first"
>
S
</font>
eries
</h1>
<p>
</p>
<table
width=
"80%"
class=
"data"
>
<tbody>
<tr>
<td
class=
"datahead"
width=
"20%"
>
Title:
</td>
<td
class=
"data"
width=
"80%"
>
Formal Puiseux Series
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Author:
</td>
<td
class=
"data"
>
<a
href=
"https://www21.in.tum.de/~eberlm"
>
Manuel Eberl
</a>
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Submission date:
</td>
<td
class=
"data"
>
2021-02-17
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
Abstract:
</td>
<td
class=
"abstract mathjax_process"
>
<p>
Formal Puiseux series are generalisations of formal power
series and formal Laurent series that also allow for fractional
exponents. They have the following general form: \[\sum_{i=N}^\infty
a_{i/d} X^{i/d}\] where
<em>
N
</em>
is an integer and
<em>
d
</em>
is a positive integer.
</p>
<p>
This
entry defines these series including their basic algebraic properties.
Furthermore, it proves the Newton–Puiseux Theorem, namely that the
Puiseux series over an algebraically closed field of characteristic 0
are also algebraically closed.
</p></td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
BibTeX:
</td>
<td
class=
"formatted"
>
<pre>
@article{Formal_Puiseux_Series-AFP,
author = {Manuel Eberl},
title = {Formal Puiseux Series},
journal = {Archive of Formal Proofs},
month = feb,
year = 2021,
note = {\url{https://isa-afp.org/entries/Formal_Puiseux_Series.html},
Formal proof development},
ISSN = {2150-914x},
}
</pre>
</td>
</tr>
<tr><td
class=
"datahead"
>
License:
</td>
<td
class=
"data"
><a
href=
"http://isa-afp.org/LICENSE"
>
BSD License
</a></td></tr>
<tr><td
class=
"datahead"
>
Depends on:
</td>
<td
class=
"data"
><a
href=
"Polynomial_Interpolation.html"
>
Polynomial_Interpolation
</a>
</td></tr>
</tbody>
</table>
<p></p>
<table
class=
"links"
>
<tbody>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Formal_Puiseux_Series/outline.pdf"
>
Proof outline
</a><br>
<a
href=
"../browser_info/current/AFP/Formal_Puiseux_Series/document.pdf"
>
Proof document
</a>
</td>
</tr>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Formal_Puiseux_Series/index.html"
>
Browse theories
</a>
</td></tr>
<tr>
<td
class=
"links"
>
<a
href=
"../release/afp-Formal_Puiseux_Series-current.tar.gz"
>
Download this entry
</a>
</td>
</tr>
<tr><td
class=
"links"
>
Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script
src=
"../jquery.min.js"
></script>
<script
src=
"../script.js"
></script>
</body>
</html>
\ No newline at end of file
web/entries/Polynomial_Interpolation.html
View file @
cb1f24a0
...
...
@@ -149,7 +149,7 @@ division of integers in target languages.</td>
<td
class=
"data"
><a
href=
"Sqrt_Babylonian.html"
>
Sqrt_Babylonian
</a>
</td></tr>
<tr><td
class=
"datahead"
>
Used by:
</td>
<td
class=
"data"
><a
href=
"Deep_Learning.html"
>
Deep_Learning
</a>
,
<a
href=
"Gauss_Sums.html"
>
Gauss_Sums
</a>
,
<a
href=
"Polynomial_Factorization.html"
>
Polynomial_Factorization
</a>
</td></tr>
<td
class=
"data"
><a
href=
"Deep_Learning.html"
>
Deep_Learning
</a>
,
<a
href=
"Formal_Puiseux_Series.html"
>
Formal_Puiseux_Series
</a>
,
<a
href=
"Gauss_Sums.html"
>
Gauss_Sums
</a>
,
<a
href=
"Polynomial_Factorization.html"
>
Polynomial_Factorization
</a>
</td></tr>
...
...
web/index.html
View file @
cb1f24a0
...
...
@@ -88,6 +88,14 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<tr>
<td
class=
"head"
>
2021
</td>
</tr>
<tr>
<td
class=
"entry"
>
2021-02-17:
<a
href=
"entries/Formal_Puiseux_Series.html"
>
Formal Puiseux Series
</a>
<br>
Author:
<a
href=
"https://www21.in.tum.de/~eberlm"
>
Manuel Eberl
</a>
</td>
</tr>
<tr>
<td
class=
"entry"
>
2021-02-10:
<a
href=
"entries/Laws_of_Large_Numbers.html"
>
The Laws of Large Numbers
</a>
...
...
web/rss.xml
View file @
cb1f24a0
...
...
@@ -9,7 +9,24 @@
and larger scientific developments, mechanically checked
in the theorem prover Isabelle.
</description>
<pubDate>
10 Feb 2021 00:00:00 +0000
</pubDate>
<pubDate>
17 Feb 2021 00:00:00 +0000
</pubDate>
<item>
<title>
Formal Puiseux Series
</title>
<link>
https://www.isa-afp.org/entries/Formal_Puiseux_Series.html
</link>
<guid>
https://www.isa-afp.org/entries/Formal_Puiseux_Series.html
</guid>
<dc:creator>
Manuel Eberl
</dc:creator>
<pubDate>
17 Feb 2021 00:00:00 +0000
</pubDate>
<description>
<
p
>
Formal Puiseux series are generalisations of formal power
series and formal Laurent series that also allow for fractional
exponents. They have the following general form: \[\sum_{i=N}^\infty
a_{i/d} X^{i/d}\] where
<
em
>
N
<
/em
>
is an integer and
<
em
>
d
<
/em
>
is a positive integer.
<
/p
>
<
p
>
This
entry defines these series including their basic algebraic properties.
Furthermore, it proves the Newton–Puiseux Theorem, namely that the
Puiseux series over an algebraically closed field of characteristic 0
are also algebraically closed.
<
/p
>
</description>
</item>
<item>
<title>
The Laws of Large Numbers
</title>
<link>
https://www.isa-afp.org/entries/Laws_of_Large_Numbers.html
</link>
...
...
@@ -584,49 +601,5 @@ development, we present the verified checker Pastèque that is obtained
by synthesis via the Refinement Framework. This is the formalization
going with our FMCAD
'
20 tool presentation.
</description>
</item>
<item>
<title>
Some classical results in inductive inference of recursive functions
</title>
<link>
https://www.isa-afp.org/entries/Inductive_Inference.html
</link>
<guid>
https://www.isa-afp.org/entries/Inductive_Inference.html
</guid>
<dc:creator>
Frank J. Balbach
</dc:creator>
<pubDate>
31 Aug 2020 00:00:00 +0000
</pubDate>
<description>
<
p
>
This entry formalizes some classical concepts and results
from inductive inference of recursive functions. In the basic setting
a partial recursive function (
"
strategy
"
) must identify
(
"
learn
"
) all functions from a set (
"
class
"
) of
recursive functions. To that end the strategy receives more and more
values $f(0), f(1), f(2), \ldots$ of some function $f$ from the given
class and in turn outputs descriptions of partial recursive functions,
for example, Gödel numbers. The strategy is considered successful if
the sequence of outputs (
"
hypotheses
"
) converges to a
description of $f$. A class of functions learnable in this sense is
called
"
learnable in the limit
"
. The set of all these
classes is denoted by LIM.
<
/p
>
<
p
>
Other types of
inference considered are finite learning (FIN), behaviorally correct
learning in the limit (BC), and some variants of LIM with restrictions
on the hypotheses: total learning (TOTAL), consistent learning (CONS),
and class-preserving learning (CP). The main results formalized are
the proper inclusions $\mathrm{FIN} \subset \mathrm{CP} \subset
\mathrm{TOTAL} \subset \mathrm{CONS} \subset \mathrm{LIM} \subset
\mathrm{BC} \subset 2^{\mathcal{R}}$, where $\mathcal{R}$ is the set
of all total recursive functions. Further results show that for all
these inference types except CONS, strategies can be assumed to be
total recursive functions; that all inference types but CP are closed
under the subset relation between classes; and that no inference type
is closed under the union of classes.
<
/p
>
<
p
>
The above
is based on a formalization of recursive functions heavily inspired by
the
<
a
href=
"
https://www.isa-afp.org/entries/Universal_Turing_Machine.html
">
Universal
Turing Machine
<
/a
>
entry by Xu et al., but different in that it
models partial functions with codomain
<
em
>
nat
option
<
/em
>
. The formalization contains a construction of a
universal partial recursive function, without resorting to Turing
machines, introduces decidability and recursive enumerability, and
proves some standard results: existence of a Kleene normal form, the
<
em
>
s-m-n
<
/em
>
theorem, Rice
'
s theorem, and assorted
fixed-point theorems (recursion theorems) by Kleene, Rogers, and
Smullyan.
<
/p
>
</description>
</item>
</channel>
</rss>
web/statistics.html
View file @
cb1f24a0
This diff is collapsed.
Click to expand it.
web/topics.html
View file @
cb1f24a0
...
...
@@ -697,6 +697,7 @@
<a
href=
"entries/Hybrid_Systems_VCs.html"
>
Hybrid_Systems_VCs
</a>
<a
href=
"entries/Subset_Boolean_Algebras.html"
>
Subset_Boolean_Algebras
</a>
<a
href=
"entries/Power_Sum_Polynomials.html"
>
Power_Sum_Polynomials
</a>
<a
href=
"entries/Formal_Puiseux_Series.html"
>
Formal_Puiseux_Series
</a>
<a
href=
"entries/Matrices_for_ODEs.html"
>
Matrices_for_ODEs
</a>
<a
href=
"entries/Smith_Normal_Form.html"
>
Smith_Normal_Form
</a>
</div>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment