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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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