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

Migrate models along inclusions of theories #374

Open
epatters opened this issue Feb 4, 2025 · 1 comment
Open

Migrate models along inclusions of theories #374

epatters opened this issue Feb 4, 2025 · 1 comment
Assignees
Labels
core Rust core for categorical logic and general computation enhancement New feature or request frontend TypeScript frontend and Rust-wasm integrations strategic Design/architecture work and prior discussion required

Comments

@epatters
Copy link
Member

epatters commented Feb 4, 2025

This issue is the first in a series about interoperating models in different logics.

As the simplest case of model migration, it should be possible to push forward a model along an inclusion of one theory into another, such as the inclusion of the base theory for causal loop diagrams (CLDs) into a theory for CLDs with extra gadgets. At the data structure level in catlog, this should be as easy changing the model's pointer to its theory, but it will take more thinking and work to:

  • decide whether all inclusions are allowed or only an explicit list of them
  • if the former, decide when and where to enumerate the inclusions
  • integrate this feature into the frontend, most likely by allow the theory selection widget to operate with a list of allowed target theories
@epatters epatters added core Rust core for categorical logic and general computation enhancement New feature or request frontend TypeScript frontend and Rust-wasm integrations tactical Typical engineering complexity labels Feb 4, 2025
@epatters epatters moved this to Ready in CatColab v0.3 Feb 4, 2025
@epatters
Copy link
Member Author

epatters commented Feb 4, 2025

My current thinking is that the inclusions should be listed explicitly in the frontend metadata because:

  • we can continue to lazy load the theories as they're selected, rather than having to load them all into memory in order to check for inclusions
  • a monomorphism between two theories need not be unique, so we'll have to explicitly give the blessed non-inclusion monomorphisms anyway (cf. Migrate models along monomorphisms of theories #375)

@epatters epatters added strategic Design/architecture work and prior discussion required and removed tactical Typical engineering complexity labels Feb 4, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
core Rust core for categorical logic and general computation enhancement New feature or request frontend TypeScript frontend and Rust-wasm integrations strategic Design/architecture work and prior discussion required
Projects
Status: Ready
Development

No branches or pull requests

2 participants