Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Application of s-finite kernels to program semantics #912

Draft
wants to merge 30 commits into
base: master
Choose a base branch
from

Conversation

affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Apr 27, 2023

Motivation for this change

This draft PR is an application of s-finite kernels to probabilistic programs.
It provides a semantics, an intrinsically-typed syntax, and a denotational semantics,

The semantics is explained in the second part of the following paper https://dl.acm.org/doi/10.1145/3573105.3575691 .

It is based on a hierarchy of kernels and its theory introduced by PR #896 (merged).
(This hierarchy is explained in the first part of the above paper.)
(NB: Originally, both the hierarchy of kernels and its application to program semantics
appeared as PR #749 (scheduled for closing) that we have split for convenience.)

The syntax is explained in this paper https://link.springer.com/chapter/10.1007/978-981-99-8311-7_9

@CohenCyril @AyumuSaito

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers
Compatibility with MathComp 2.0
  • I added the label TODO: HB port to make sure someone ports this PR to
    the hierarchy-builder branch or I already opened an issue or PR (please cross reference).
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

@affeldt-aist affeldt-aist marked this pull request as draft April 27, 2023 03:57
@affeldt-aist affeldt-aist added the experiment 🧪 This issue/PR is very experimental label Apr 27, 2023
This was referenced Apr 27, 2023
@affeldt-aist affeldt-aist changed the title Prob lang Application of s-finite kernels to program semantics Apr 27, 2023
@affeldt-aist affeldt-aist mentioned this pull request Apr 27, 2023
3 tasks
@affeldt-aist affeldt-aist force-pushed the prob_lang branch 3 times, most recently from 870c929 to 1a34645 Compare May 22, 2023 00:11
@affeldt-aist affeldt-aist force-pushed the prob_lang branch 3 times, most recently from 8dc09a2 to 6242813 Compare August 22, 2023 02:42
@affeldt-aist affeldt-aist force-pushed the prob_lang branch 2 times, most recently from e4c675f to 564ae22 Compare November 17, 2023 05:20
@affeldt-aist affeldt-aist force-pushed the prob_lang branch 2 times, most recently from 4a191b6 to 00feb59 Compare January 9, 2024 04:46
@affeldt-aist affeldt-aist force-pushed the prob_lang branch 3 times, most recently from cc2f275 to 5d96668 Compare April 30, 2024 16:23
@affeldt-aist affeldt-aist force-pushed the prob_lang branch 2 times, most recently from 5e78cea to 5aecc7f Compare July 29, 2024 13:01
@affeldt-aist affeldt-aist force-pushed the prob_lang branch 2 times, most recently from 48c890c to bfb2fc6 Compare August 8, 2024 13:45
AyumuSaito and others added 29 commits October 24, 2024 11:41
Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
- binomial
- uniform
- generalize measure_and
- change the order of binop & add pow
- fix for mR
- rewrite casino0 to casino1

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
- also fix casino1
- several admits proved
- patch
- admits in examples wip
Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
- define beta_probability
- proof beta_ge0
- add exp_beta
- clean up def of beta
- beta_nat_bern_bern
- rewrite casino01
- proved casino34'
- casino34 (remain admit)
- casino45
- add Normalize
- use change of variables from charge.v
  to prove lemma integral_beta_nat (wip)
- beta_nat_bern_bern
- new version of Bernoulli
- cleaning
- beta_nat_norm_sym
- generic change variables
- beta_nat_normE
- complete the casion example
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
experiment 🧪 This issue/PR is very experimental
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants