0
$\begingroup$

This library “generates all models of a first order theory”: https://github.com/andrejbauer/alg

Is it able to take the formal semantics of a programming language, like:

and generate all possible expressions / valid sequences of commands, under some length limit, k? What does a preparation of the specification of the language look like, for use in alg?

Improve this question
$\endgroup$
2
  • $\begingroup$ Does "possible expressions" count as models? $\endgroup$
    – Trebor ♦
    Commented Jun 10, 2023 at 3:26
  • $\begingroup$ I have no idea, let me know what you think please. I think I should just study Knuth’s chapters on induction since that is I think what I am obsessed with. math.stackexchange.com/questions/1601798/… $\endgroup$
    – Julius Hamilton
    Commented Jun 16, 2023 at 12:35

1 Answer 1

Reset to default
3
$\begingroup$

Theoretically speaking, it might be possible because Alg can axiomatize any single-sorted first-order theory with equality. It's not clear to me how to do it directly, though.

Practically speaking, you would get a horribly inefficient thing that wouldn't get anywhere. Alg is not meant for this sort of thing.

You're probably better off looking at logic programming, except you'd want breadth-first search rather than depth-first. Perhaps someone knows of a prolog-like program that can do breadth-first search? Maybe a modern prolog implementation?

Improve this answer
$\endgroup$
2

Not the answer you're looking for? Browse other questions tagged or ask your own question.