Formulog: ML + Datalog + SMT

#1

Post by matt_d » Sat, Aug 08, 2020, 12:23 PM UTC

Formulog: ML + Datalog + SMT
weaselhat.com

Re: Formulog: ML + Datalog + SMT

#2

Post by siraben » Sat, Aug 08, 2020, 2:08 PM UTC

There's a reason why a lot of programming language papers use formal math notation, because it's a lot more concise to express the entire typing rules of your language in a dozen or so inference rules rather than a more convoluted implementation.[0]

Formulog looks like it could potentially replace that math notation for something as rigorous yet executable.

On the other hand, denotational semantics are usually straightforward enough to be implemented by reading off the math. As an example, it was quite easy for me to translate Scheme's semantics to code.[1]

I hope it gets reimplemented in a functional language as well, Formulog's current implementation is in Java[2] which might not be ideal for reducing implementation bugs.

[0] Contrast the code and math: https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf

[1] https://github.com/siraben/r5rs-denot

[2] https://github.com/HarvardPL/formulog

Re: Formulog: ML + Datalog + SMT

#3

Post by Ericson2314 » Sat, Aug 08, 2020, 2:28 PM UTC

It is also integesting to see how typeclasses/traits and OCaml's (still upcoming?) "modular implicits" are related to logic programming.

I commend the rustc team for taking this lineage seriously in developing Chalk[1] and using differential-dataflow for the next borrow checker. If they combine those into a differential-dataflow-powered Chalk it will be very formidable!

We'll have to catch up Haskell at some point, sigh.

[1]: https://github.com/rust-lang/chalk.git

[2]: https://github.com/TimelyDataflow/differential-dataflow

Re: Formulog: ML + Datalog + SMT

#4

Post by benrbray » Sat, Aug 08, 2020, 2:39 PM UTC

siraben wrote: post #2

There's a reason why a lot of programming language papers use formal math notation, because it's a lot more concise to express the entire typing rules of your language in a dozen or so inference rules rather than a more convoluted implementation.[0] Formulog looks like it could potentially replace that math notation for something as rigorous yet executable. On the other hand, denotational semantics are usually straig…

Any advice for learning to read the PL math notation? The PL papers I've seen normally take it for granted, so I don't even know what it's called to search for it!

EDIT: Thank you all for the references :)

Re: Formulog: ML + Datalog + SMT

#5

Post by siraben » Sat, Aug 08, 2020, 2:49 PM UTC

benrbray wrote: post #4

siraben wrote: post #2

There's a reason why a lot of programming language papers use formal math notation, because it's a lot more concise to express the entire typing rules of your language in a dozen or so inference rules rather than a more convoluted implementation.[0] Formulog looks like it could potentially replace that math notation for something as rigorous yet executable. On the other hand, denotational semantics are usually straig…

Any advice for learning to read the PL math notation? The PL papers I've seen normally take it for granted, so I don't even know what it's called to search for it! EDIT: Thank you all for the references :)

If you're talking about the inference rules used to specify the type system of a programming language, one of Wikipedia's[0] references is[1] which from a quick skim seems adequate. The main takeaway is that the things above the line are the assumptions, and the things below the line is what you conclude. Γ is usually used for typing environments (a map from variables to their types), the turnstile ⊢ can be read as "from the context on the left, it entails the typing information on the right". As a quick example:

  Γ ⊢ e1 : Int    Γ ⊢ e2 : Int 
  ----------------------------
       Γ ⊢ e1 + e2 : Int

Which reads, if e1 has type Int in Γ, and e2 has type Int in Γ, then e1 + e2 also has type Int in Γ. These rules are really bidirectional which is what allows you to perform typechecking. If you have an expression (a + b) of type Int, you can reduce it into two subproblems, typechecking a expecting an Int, and similarly for b.

[0] https://en.wikipedia.org/wiki/Type_rule

[1] https://www.cs.colorado.edu/~bec/courses/csci5535/reading/ca...

Re: Formulog: ML + Datalog + SMT

#6

Post by matt_d » Sat, Aug 08, 2020, 3:37 PM UTC

benrbray wrote: post #4

siraben wrote: post #2

There's a reason why a lot of programming language papers use formal math notation, because it's a lot more concise to express the entire typing rules of your language in a dozen or so inference rules rather than a more convoluted implementation.[0] Formulog looks like it could potentially replace that math notation for something as rigorous yet executable. On the other hand, denotational semantics are usually straig…

Any advice for learning to read the PL math notation? The PL papers I've seen normally take it for granted, so I don't even know what it's called to search for it! EDIT: Thank you all for the references :)

I can recommend the references listed in "Background: Notation" section of Program Analysis Resources: https://gist.github.com/MattPD/00573ee14bf85ccac6bed3c0678dd...

Re: Formulog: ML + Datalog + SMT

#7

Post by mgreenbe » Sat, Aug 08, 2020, 3:45 PM UTC

siraben wrote: post #5

benrbray wrote: post #4

Earlier quoted context omitted.

Any advice for learning to read the PL math notation? The PL papers I've seen normally take it for granted, so I don't even know what it's called to search for it! EDIT: Thank you all for the references :)

If you're talking about the inference rules used to specify the type system of a programming language, one of Wikipedia's[0] references is[1] which from a quick skim seems adequate. The main takeaway is that the things above the line are the assumptions, and the things below the line is what you conclude. Γ is usually used for typing environments (a map from variables to their types), the turnstile ⊢ can be read as "…

Re: Formulog: ML + Datalog + SMT

#8

Post by gmfawcett » Sat, Aug 08, 2020, 3:51 PM UTC

benrbray wrote: post #4

siraben wrote: post #2

There's a reason why a lot of programming language papers use formal math notation, because it's a lot more concise to express the entire typing rules of your language in a dozen or so inference rules rather than a more convoluted implementation.[0] Formulog looks like it could potentially replace that math notation for something as rigorous yet executable. On the other hand, denotational semantics are usually straig…

Any advice for learning to read the PL math notation? The PL papers I've seen normally take it for granted, so I don't even know what it's called to search for it! EDIT: Thank you all for the references :)

Also try searching for "sequent calculus" or "Gentzen proof calculus" which describe the underlying logical framework.

You might enjoy this tutorial: http://logitext.mit.edu/logitext.fcgi/tutorial

Re: Formulog: ML + Datalog + SMT

#9

Post by remexre » Sat, Aug 08, 2020, 3:52 PM UTC

benrbray wrote: post #4

siraben wrote: post #2

There's a reason why a lot of programming language papers use formal math notation, because it's a lot more concise to express the entire typing rules of your language in a dozen or so inference rules rather than a more convoluted implementation.[0] Formulog looks like it could potentially replace that math notation for something as rigorous yet executable. On the other hand, denotational semantics are usually straig…

Any advice for learning to read the PL math notation? The PL papers I've seen normally take it for granted, so I don't even know what it's called to search for it! EDIT: Thank you all for the references :)

And if you're fine with something much longer than others have suggested, Types And Programming Languages [0] covers the notation, in addition to most of the other knowledge most PL papers take for granted.

[0]: https://www.cis.upenn.edu/~bcpierce/tapl/

Re: Formulog: ML + Datalog + SMT

#10

Post by guerrilla » Sat, Aug 08, 2020, 4:01 PM UTC

gmfawcett wrote: post #8

benrbray wrote: post #4

Earlier quoted context omitted.

Any advice for learning to read the PL math notation? The PL papers I've seen normally take it for granted, so I don't even know what it's called to search for it! EDIT: Thank you all for the references :)

Also try searching for "sequent calculus" or "Gentzen proof calculus" which describe the underlying logical framework. You might enjoy this tutorial: http://logitext.mit.edu/logitext.fcgi/tutorial

Dag Prawitz's book "Natural Deduction" isn't too hard to read .