Skip to content
This repository has been archived by the owner on Jun 1, 2022. It is now read-only.

Termination checking #611

Open
jonhue opened this issue Mar 19, 2021 · 0 comments
Open

Termination checking #611

jonhue opened this issue Mar 19, 2021 · 0 comments
Labels
analyze The analyze component comprises exploring the AST to find dependencies and build a symbol table enhancement New feature or request type inference During type inference the types of nodes in the AST are inferred

Comments

@jonhue
Copy link
Member

jonhue commented Mar 19, 2021 •
edited
Loading

Introduce a separate type (called bottom) representing the type of (potentially) non-terminating expressions. Automatically prove some expressions to be terminating and add or remove this type accordingly.

Investigate also distinguishing total and partial functions (-> relation to refinement types)

See https://agda.readthedocs.io/en/v2.6.1/language/termination-checking.html, https://arxiv.org/pdf/1012.4900.pdf.
@jonhue jonhue added enhancement New feature or request analyze The analyze component comprises exploring the AST to find dependencies and build a symbol table type inference During type inference the types of nodes in the AST are inferred labels Mar 19, 2021
@jonhue jonhue added this to Core Nov 19, 2021
@jonhue jonhue moved this to Todo in Core Nov 19, 2021
@jonhue jonhue moved this from Todo to Processing in Core Nov 19, 2021
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
analyze The analyze component comprises exploring the AST to find dependencies and build a symbol table enhancement New feature or request type inference During type inference the types of nodes in the AST are inferred
Projects
Core
Status: Processing
Milestone
No milestone
Development

No branches or pull requests
1 participant
@jonhue