On Abstract Machine Semantics for Proto-Quipper-M
- URL: http://arxiv.org/abs/2105.03522v1
- Date: Fri, 7 May 2021 22:16:11 GMT
- Title: On Abstract Machine Semantics for Proto-Quipper-M
- Authors: Andrea Colledan
- Abstract summary: Quipper is a domain-specific programming language for the description of quantum circuits.
Because it is implemented as an embedded language in Haskell, Quipper is a very practical functional language.
Because Haskell lacks linear types, it is easy to write Quipper programs that violate the non-cloning property of quantum states.
- Score: 0.0
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Quipper is a domain-specific programming language for the description of
quantum circuits. Because it is implemented as an embedded language in Haskell,
Quipper is a very practical functional language. However, for the same reason,
it lacks a formal semantics and it is limited by Haskell's type system. In
particular, because Haskell lacks linear types, it is easy to write Quipper
programs that violate the non-cloning property of quantum states. In order to
formalize relevant fragments of Quipper in a type-safe way, the Proto-Quipper
family of research languages has been introduced over the last years. In this
paper we first review Proto-Quipper-M, an instance of the Proto-Quipper family
based on a categorical model for quantum circuits, which features a linear type
system that guarantees that the non-cloning property holds at compile time. We
then derive a tentative small-step operational semantics from the big-step
semantics of Proto-Quipper-M and we prove that the two are equivalent. After
proving subject reduction and progress results for the tentative semantics, we
build upon it to obtain a truly small-step semantics in the style of an
abstract machine, which we eventually prove to be equivalent to the original
semantics.
Related papers
- Dictionary Learning Improves Patch-Free Circuit Discovery in Mechanistic
Interpretability: A Case Study on Othello-GPT [59.245414547751636]
We propose a circuit discovery framework alternative to activation patching.
Our framework suffers less from out-of-distribution and proves to be more efficient in terms of complexity.
We dig in a small transformer trained on a synthetic task named Othello and find a number of human-understandable fine-grained circuits inside of it.
arXiv Detail & Related papers (2024-02-19T15:04:53Z) - Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
We propose Chain of Code, a simple yet surprisingly effective extension that improves LM code-driven reasoning.
The key idea is to encourage LMs to format semantic sub-tasks in a program as flexible pseudocode that the interpreter can explicitly catch.
arXiv Detail & Related papers (2023-12-07T17:51:43Z) - LINC: A Neurosymbolic Approach for Logical Reasoning by Combining
Language Models with First-Order Logic Provers [60.009969929857704]
Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society.
In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC.
We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
arXiv Detail & Related papers (2023-10-23T17:58:40Z) - OrdinalCLIP: Learning Rank Prompts for Language-Guided Ordinal
Regression [94.28253749970534]
We propose to learn the rank concepts from the rich semantic CLIP latent space.
OrdinalCLIP consists of learnable context tokens and learnable rank embeddings.
Experimental results show that our paradigm achieves competitive performance in general ordinal regression tasks.
arXiv Detail & Related papers (2022-06-06T03:54:53Z) - A Paradigm Change for Formal Syntax: Computational Algorithms in the
Grammar of English [0.0]
We turn to programming languages as models for a process-based syntax of English.
The combination of a functional word and a content word was chosen as the topic of modeling.
The fit of the model was tested by deriving three functional characteristics crucial for the algorithm and checking their presence in English grammar.
arXiv Detail & Related papers (2022-05-24T07:28:47Z) - Proto-Quipper with dynamic lifting [1.5274311118568713]
We extend Proto-Quipper-M with a construct called dynamic lifting, which is present in Quipper.
Dynamic lifting enables Proto-Quipper programs to interleave classical and quantum computation.
arXiv Detail & Related papers (2022-04-27T16:34:15Z) - On Dynamic Lifting and Effect Typing in Circuit Description Languages
(Extended Version) [0.0]
We introduce a generalization of the paradigmatic-calculus Proto-Quipper-M, itself modeling the core features of the quantum circuit description language Quipper.
The extension, called Proto-Quipper-K, is meant to capture a very general form of dynamic lifting.
arXiv Detail & Related papers (2022-02-15T18:33:41Z) - RNNs can generate bounded hierarchical languages with optimal memory [113.73133308478612]
We show that RNNs can efficiently generate bounded hierarchical languages that reflect the scaffolding of natural language syntax.
We introduce Dyck-($k$,$m$), the language of well-nested brackets (of $k$ types) and $m$-bounded nesting depth.
We prove that an RNN with $O(m log k)$ hidden units suffices, an exponential reduction in memory, by an explicit construction.
arXiv Detail & Related papers (2020-10-15T04:42:29Z) - A tutorial introduction to quantum circuit programming in dependently
typed Proto-Quipper [1.5274311118568713]
We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types.
We show how dependent types enable programming families of circuits, and how dependent types solve the problem of type-safe uncomputation of garbage qubits.
arXiv Detail & Related papers (2020-05-17T23:31:23Z) - A Tale of a Probe and a Parser [74.14046092181947]
Measuring what linguistic information is encoded in neural models of language has become popular in NLP.
Researchers approach this enterprise by training "probes" - supervised models designed to extract linguistic structure from another model's output.
One such probe is the structural probe, designed to quantify the extent to which syntactic information is encoded in contextualised word representations.
arXiv Detail & Related papers (2020-05-04T16:57:31Z) - Linear Dependent Type Theory for Quantum Programming Languages [1.7166794984161973]
Modern quantum programming languages integrate quantum resources and classical control.
They must be linearly typed to reflect the no-cloning property of quantum resources.
High-level and practical languages should also support quantum circuits as first-class citizens.
arXiv Detail & Related papers (2020-04-28T13:11:06Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.