DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2022.28

Deeper Shallow Embeddings

Authors: Jacob Prinz, G. A. Kavvos, and Leonidas Lampropoulos

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract

Deep and shallow embeddings are two popular techniques for embedding a language in a host language with complementary strengths and weaknesses. In a deep embedding, embedded constructs are defined as data in the host: this allows for syntax manipulation and facilitates metatheoretic reasoning, but is challenging to implement - especially in the case of dependently typed embedded languages. In a shallow embedding, by contrast, constructs are encoded using features of the host: this makes them quite straightforward to implement, but limits their use in practice. In this paper, we attempt to bridge the gap between the two, by presenting a general technique for extending a shallow embedding of a type theory with a deep embedding of its typing derivations. Such embeddings are almost as straightforward to implement as shallow ones, but come with capabilities traditionally associated with deep ones. We demonstrate these increased capabilities in a number of case studies; including a DSL that only holds affine terms, and a dependently typed core language with computational beta reduction that leverages function extensionality.

Cite as

Jacob Prinz, G. A. Kavvos, and Leonidas Lampropoulos. Deeper Shallow Embeddings. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{prinz_et_al:LIPIcs.ITP.2022.28,
  author =	{Prinz, Jacob and Kavvos, G. A. and Lampropoulos, Leonidas},
  title =	{{Deeper Shallow Embeddings}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.28},
  URN =		{urn:nbn:de:0030-drops-167379},
  doi =		{10.4230/LIPIcs.ITP.2022.28},
  annote =	{Keywords: type theory, shallow embedding, deep embedding, Agda}
}

Document

DOI: 10.4230/LIPIcs.FUN.2018.15

A Muffin-Theorem Generator

Authors: Guangqi Cui, John Dickerson, Naveen Durvasula, William Gasarch, Erik Metz, Jacob Prinz, Naveen Raman, Daniel Smolyak, and Sung Hyun Yoo

Published in: LIPIcs, Volume 100, 9th International Conference on Fun with Algorithms (FUN 2018)

Abstract

Consider the following FUN problem. Given m,s you want to divide m muffins among s students so that everyone gets m/(s) muffins; however, you want to maximize the minimum piece so that nobody gets crumbs. Let f(m,s) be the size of the smallest piece in an optimal procedure. We study the case where ceil(2m/s)=3 because (1) many of our hardest open problems were of this form until we found this method, (2) we have used the technique to generate muffin-theorems, and (3) we conjecture this can be used to solve the general case. We give (1) an algorithm to find an upper bound for f(m,s) when ceil(2m/s)(and some ways to speed up that algorithm if certain conjectures are true), (2) an algorithm that uses the information from (1) to try to find a lower bound on f(m,s) (a procedure) which matches the upper bound, (3) an algorithm that uses the information from (1) to generate muffin-theorems, and (4) an algorithm that we think works well in practice to find f(m,s) for any m,s.

Cite as

Guangqi Cui, John Dickerson, Naveen Durvasula, William Gasarch, Erik Metz, Jacob Prinz, Naveen Raman, Daniel Smolyak, and Sung Hyun Yoo. A Muffin-Theorem Generator. In 9th International Conference on Fun with Algorithms (FUN 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 100, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{cui_et_al:LIPIcs.FUN.2018.15,
  author =	{Cui, Guangqi and Dickerson, John and Durvasula, Naveen and Gasarch, William and Metz, Erik and Prinz, Jacob and Raman, Naveen and Smolyak, Daniel and Yoo, Sung Hyun},
  title =	{{A Muffin-Theorem Generator}},
  booktitle =	{9th International Conference on Fun with Algorithms (FUN 2018)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-067-5},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{100},
  editor =	{Ito, Hiro and Leonardi, Stefano and Pagli, Linda and Prencipe, Giuseppe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FUN.2018.15},
  URN =		{urn:nbn:de:0030-drops-88062},
  doi =		{10.4230/LIPIcs.FUN.2018.15},
  annote =	{Keywords: Fair Division, Theorem Generation}
}

Search Results

Documents authored by Prinz, Jacob

Deeper Shallow Embeddings

Abstract

Cite as

A Muffin-Theorem Generator

Abstract

Cite as

Thanks for your feedback!

Could not send message