Trees for Logic and Parsing in C++ - Hans de Nivelle - CppNow 2023
https://www.cppnow.org
/ cppnow
---
Trees for Logic and Parsing in C++ - Hans de Nivelle - CppNow 2023
Slides: https://github.com/boostcon
---
The motivation of this session is the implementation of logic in C++. When I say 'logic', I mean 'formal logic', as in lambda calculus, type theory, or higher-order logic.
Logic uses recursively defined trees with different constructors of different forms. This makes construction, inspection, and replacement of subtrees difficult.
Functional languages may appear more suitable for implementing logic because they have a logical foundation. I will try to convince you that, when done right, the necessary recursive tree-types can be implemented equally nicely in C++, perhaps even nicer. The interface can be clean, and easier to use than in functional languages. Construction can be done by standard constructors. Deconstruction can be done by matching, but it is not the best approach: It is better to replace matching by a combination of switch( ) and views (a form of casts)
I also describe what I believe is the most efficient implementation, minimizing pointer indirections and reallocations. (Surprise: The best implementation doesn't use variant or derived classes) Since writing the class definitions by hand is still very time-consuming, I created a generator that automatically creates a set of class definitions from a recursive definition of a tree datatype.
The result is an approach to implementing logic that is easier to use than a functional language. As a side effect, the same approach can be used for implementing abstract syntax trees (AST). This presentation is the result of +/- 15 year of trying to implement logic.
---
Hans de Nivelle
From 1999 to 2007, Hans de Nivelle worked as a full-time researcher at Max-Planck Institute for Computer Science in Saarbruecken, Germany. His research topic was automated theorem proving. This is the art of automatically finding logical proofs by a computer program. This involves search, which needs efficient implementation. He initially used C for implementating theorem provers, but switched to C++ in 2003.
After 2005, HdN became interested in verification of mathematical proofs He implemented several small interactive verification programs in C++. This was very tedious, so he tried various other languages, but he always returned to C++.
From 2007-2017, HdN was a professor at University of Wroclaw, Poland, where he continued doing research on automated theorem proving in combination with interactive theorem proving. In Wroclaw, he taught logic, theory of computation, compiler construction, flight simulation, and programming in C++.
From 2018 until present, Hans de Nivelle is professor at Nazarbayev University in Astana, Kazakhstan. During this time, he has been teaching programming in Haskell, Prolog, Java, Python, C, and C++, as well as formal language theory, complexity theory, and compiler construction. He is currently developing a new programming language specialized for implementation of logic. During the development of the compiler, he noticed that there is no suitable parser generator for C++, so he created Maphoon, which was presented last year at CppNow. While studying the problem of how to compile the programming language into C, he observed that the new techniques can also be used directly in C++. This results in the current talk. It is possible that the new implementation techniques are so convenient that the original plan of developing a programming language has become unnecessary.
---
Video Sponsors: think-cell and Bloomberg Engineering
Audience Audio Sponsors: Innoplex and Maryland Research Institute
---
Videos Filmed & Edited By Bash Films: https://bashfilms.com/
YouTube Channel Managed & Optimized By Digital Medium Ltd: https://events.digital-medium.co.uk
---
CppNow 2024
https://www.cppnow.org
/ cppnow
---
#boost #cpp #cppprogramming