cls-python

Synthesis using inhabitation in FCL with intersection types

https://github.com/tudo-seal/cls-python

Science Score: 44.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • CITATION.cff file
    Found CITATION.cff file
  • codemeta.json file
    Found codemeta.json file
  • .zenodo.json file
    Found .zenodo.json file
  • DOI references
  • Academic publication links
  • Academic email domains
  • Institutional organization owner
  • JOSS paper metadata
  • Scientific vocabulary similarity
    Low similarity (10.6%) to scientific vocabulary
Last synced: 6 months ago · JSON representation ·

Repository

Synthesis using inhabitation in FCL with intersection types

Basic Info
  • Host: GitHub
  • Owner: tudo-seal
  • License: apache-2.0
  • Language: Python
  • Default Branch: main
  • Size: 2.92 MB
Statistics
  • Stars: 0
  • Watchers: 2
  • Forks: 2
  • Open Issues: 0
  • Releases: 0
Created over 2 years ago · Last pushed almost 2 years ago
Metadata Files
Readme License Citation

README.md

(Vanilla) Combinatory Logic Synthesis in Python

This repository is a fork of cls-python. Advancements made to the core system from the boolean fork (see main branch) are backported here.

Installation

Since this project does not need any additional dependencies, you can simply clone this repository to a location, where your code can access it. In case you want to install it, you can do this by either run

pip install .

in the cloned repository, or

pip install git+https://github.com/tudo-seal/bcls-python@vanilla

without the need to clone it beforehand.

Usage

A repository is a dict, that maps Combinators to Types. A combinator can be any Hashable object. Special treatment occurs, if it is Callable. A query is a Type

Once you specified a repository gamma and a query q, you can start the inhabitation procedure by

grammar = FiniteCombinatoryLogic(gamma, Subtypes({})).inhabit(q)

Note: Subtypes can contain a priori subtype information in the form of a dict from a constructor name to a set of constructor names.

grammar contains a tree grammar that was build by the inhabitation procedure. You can access the terms, that inhabit q by

terms = enumerate_terms(q, grammar)

Note: Since the enumerated results are potentially infinite, enumerated_results returns a lazy Generator.

The last step is to evaluate the terms. This simply calls a term iff it is Callable with its assigned (and evaluated) parameters. If it is not callable, the object in itself is returned. This is useful for constants like simple strings or numbers.

for term in terms:
    do_sth_with(interpret_term(term))

See the examples on how to construct repositories, combinators and queries.

Owner

  • Name: SEAL - Software Engineering by Algorithms and Logic
  • Login: tudo-seal
  • Kind: organization

Citation (CITATION.cff)

# This CITATION.cff file was generated with cffinit.
# Visit https://bit.ly/cffinit to generate yours today!

cff-version: 1.2.0
title: CLS-Python
message: >-
  If you use this software, please cite it using the
  metadata from this file.
type: software
authors:
  - given-names: Christoph
    family-names: Stahl
    email: christoph.stahl@tu-dortmund.de
    affiliation: TU Dortmund University
    orcid: 'https://orcid.org/0009-0006-9079-8379'
  - given-names: Andrej
    family-names: Dudenhefner
    email: andrej.dudenhefner@cs.tu-dortmund.de
    affiliation: TU Dortmund University
    orcid: 'https://orcid.org/0000-0003-1104-444X'
  - given-names: Jan
    family-names: Bessai
    email: jan.bessai@tu-dortmund.de
repository-code: 'https://github.com/tudo-seal/cls-python'
keywords:
  - combinatory logic
  - type system
  - inhabitation
  - intersection types
  - program synthesis
license: Apache-2.0

GitHub Events

Total
Last Year

Dependencies

.github/workflows/python-app.yml actions
  • actions/checkout v3 composite
  • actions/setup-python v4 composite
  • jpetrucciani/ruff-check main composite
pyproject.toml pypi
  • python ^3.10