COQ'S FUNCTIONAL PROGRAMMING LANGUAGE

REVISED: Tuesday, November 5, 2024

1. COQ'S FUNCTIONAL PROGRAMMING LANGUAGE

We type in the CoqIDF buffer window using Coq keyword vernacular commands.

As shown below, the Inductive type day : is defined to be := the list of day items or constructors separated by | vertical bars. The list of constructors ends with a period .

Inductive day : Type :=

    | monday

    | tuesday

    | wednesday

    | thursday

    | friday

    | saturday

    | sunday.

We move the cursor to the right of the period and click the CoqIDE down-arrow to compile the above Type.  If the compile is successful the line color changes to green.

After the successful compile, CoqIDE responds in the Messages' window with 

day is defined

day_rect is defined

day_ind is defined

day_rec is defined

day_sind is defined

Next, we write the function next_weekday based on the above day type. The function uses pattern matching, matching the argument d and the branch or case type it returns will be : day type. The branch or case is separated by right arrows pointing to the matching argument. The function ends with end and a period .

Definition next_weekday (d:day) : day :=

    match d with

    | monday    => tuesday

    | tuesday   => wednesday

    | wednesday => thursday

    | thursday  => friday

    | friday    => monday

    | saturday  => monday

    | sunday    => monday

    end.

We move the cursor to the right of the period after end and click the CoqIDE down-arrow to compile the function next_weekday.  If the compile is successful the function color changes to green.

After the successful compile, CoqIDE responds in the Messages' window with 

next_weekday is defined

To call a function, we use the vernacular command Compute.

Compute (next_weekday friday).

After the successful compile, CoqIDE responds in the Messages window with

    = monday

     : day

We test our next_weekday function using the vernacular command Example.

Example test_next_weekday :

    (next_weekday (next_weekday saturday)) = tuesday.

After a successful compile, CoqIDE responds in the Goal's window by telling us we must first prove the new test_next_weekday function before we can use it. 

1 goal

______________________________________(1/1)

next_weekday (next_weekday saturday) =

tuesday

CoqIDF wants us to prove 1 goal the test_next_weekday function.

We use the simpl tactic to simplify the goal we are trying to prove. 

Proof. simpl. reflexivity. Qed.

After Proof we compile period by period one at a time. After the successful compile of  simple,  CoqIDE responds in the Goal's window with 

1 goal

______________________________________(1/1)

tuesday = tuesday

Notice 1 goal has changed, now both sides of = are the same.

When both sides of = are the same we can use the tactic reflexivity. After the successful compile of  reflexivity, CoqIDE responds in the Goal's window with 

No more goals.

Now when we compile Qed. all windows are blank and CoqIDE accepts the Proof as proven.

Compute (next_weekday (next_weekday saturday)).

After the successful compile, CoqIDE responds in the Messages window with

    = tuesday

     : day

Notice the above Compute is passing function arguments from right to left. For example, next_weekday saturday computes to monday which is passed as an argument to the function on the left next_weekday which uses it to compute the final answer tuesday.

2. CONCLUSION 

The Coq functional programming Language is easy to use.

3. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

CALCULUS of INDUCTIVE CONSTRUCTIONS (CIC) and Gallina

REVISED: Wednesday, October 30, 2024

1. The Calculus of Inductive Constructions (CIC)

CIC is a powerful type of theory that serves as the foundation for the Coq proof assistant. It's a higher-order logic system where types and terms are unified, allowing for a seamless integration of logic and computation.

Key Features

Types and Terms:

In CIC, types and terms are not distinct entities. Both are represented as expressions within the same language. This means that types can be the subjects of proofs, and proofs can be the objects of computation.

Dependent Types: 

CIC supports dependent types, where the type of an expression can depend on the value of another expression. This enables fine-grained reasoning about complex data structures and algorithms.

Inductive Types: 

Inductive types allow the definition of recursive data structures, such as natural numbers, lists, and trees. This is crucial for defining algorithms and proving properties about them.

Proofs as Programs: 

The Curry-Howard isomorphism, a fundamental principle in CIC, establishes a correspondence between proofs and programs. This means that proofs can be seen as programs that construct values of a certain type, and programs can be seen as proofs of their correctness.

2. Gallina

Gallina is a high-level specification language built on top of CIC. It provides a more user-friendly syntax and a rich set of features for writing mathematical proofs and formal specifications.

Key Features

Intuitive Syntax: 

Gallina uses a more natural syntax compared to raw CIC, making it easier to read and write.

Tactics: 

Gallina provides a variety of tactics for constructing proofs interactively. These tactics automate common proof steps, reducing the amount of manual effort required.

Inductive Definitions: 

Gallina allows for the definition of inductive types and functions using a concise and intuitive syntax.

Higher-Order Logic: 

Gallina supports higher-order logic, allowing for reasoning about functions and predicates.

3. How Gallina and CIC Work Together

Key Features

Specification: 

The user writes a formal specification in Gallina, defining the properties and theorems to be proven.

Proof Development: 

The user interacts with the Coq proof assistant to construct proofs interactively. Gallina provides a convenient interface for this process.

Type Checking: 

Coq's type checker ensures the correctness of the proof by verifying that each step adheres to the rules of CIC.

Proof Completion: 

Once a proof is completed, Coq generates a formal proof object, which can be machine-checked for correctness.

4. Benefits of Using CIC and Gallina

Key Features

Formal Verification: 

CIC and Gallina enable the formal verification of software and hardware systems, ensuring their correctness and reliability.

Mathematical Reasoning: 

CIC can be used to formalize and reason about complex mathematical concepts, such as number theory, algebra, and topology.

Program Synthesis: 

The Curry-Howard isomorphism allows for the synthesis of programs from proofs, leading to the development of correct-by-construction software.

Education and Research: 

CIC and Gallina are powerful tools for teaching and researching formal methods, logic, and programming languages.

5. CONCLUSION

CIC and Gallina provide a robust framework for formal reasoning and program verification. By combining the power of higher-order logic, dependent types, and inductive definitions, they enable the development of complex mathematical theories and the rigorous verification of software systems.

6. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

COQ

REVISED: Tuesday, October 29, 2024

1. INTRODUCTION

Imagine you're building a really cool LEGO structure. You have all the bricks and pieces, and you have a plan (instructions) on how to build it. Coq is like a super smart friend who helps you make sure you're following the plan perfectly and that your LEGO structure is strong and sturdy.

Here's how it works:

Proof Assistant:

Coq is a proof assistant. That means it helps you write proofs, which are like arguments or explanations that show something is true.

Math and Programming:

Coq can be used for math and programming. In math, it can help you prove theorems, like proving that 2 + 2 always equals 4. In programming, it can help you write programs that are correct and work the way they should.

Formal Verification:

Coq is used for formal verification. This means it can check if your math or programming is correct, just like your friend checks your LEGO building.

So, Coq is a powerful tool that helps people be sure that their math and programming is accurate and reliable. It's like having a super-smart friend who can help

2. COQIDE

Imagine CoqIDE as a special kind of word processor, but instead of writing stories or essays, it helps you build logical arguments and proofs. It's like having a super smart friend who can check your work and tell you if your reasoning is correct.

Here's what it does:

Proof Editing:

You can type in your proofs, and CoqIDE will help you by suggesting steps or pointing out mistakes.

Auto-Completion: 

It can finish your sentences for you, just like your phone does when you text!

Highlighting: 

It highlights important parts of your proof to make it easier to read and understand.

Checking: 

CoqIDE checks your proof step-by-step to make sure it's logically sound.

So, CoqIDE is a tool that helps you build strong, accurate proofs. It's like having a helpful assistant who makes sure your logical thinking is top-notch.

3. COQ-SHELL

Imagine Coq-Shell as a magical text box where you can type in math problems and proofs. It's like having a super smart calculator that not only gives you answers but also checks if your thinking is correct.

Here's how it works:

Typing: 

You type in your math problems and proofs using special commands.

Checking: 

Coq-Shell checks your work step-by-step to make sure it's logically sound.

Feedback: 

It gives you feedback, like if you made a mistake or if your proof is correct.

So, Coq-Shell is a tool that helps you explore math and logic in a fun and interactive way. It's like having a math wizard by your side, guiding you through your calculations and helping you discover new things!

4. CONCLUSION

In this tutorial, you have received a brief overview of Coq, Coq-IDE, and Coq-Shell.

5. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL TO AGDA AND COQ

 

REVISED: Thursday, October 31, 2024

1. INTRODUCTION

As software systems become more complex and critical, the demand for rigorous verification methods will grow. Agda and Coq, with their ability to formally prove the correctness of programs, are well-positioned to play a significant role in this domain.

These languages are excellent tools for teaching and research in computer science and mathematics. They provide a solid foundation for understanding complex concepts and developing formal reasoning skills.

Agda and Coq's strengths in expressing complex specifications and proofs make them suitable for specialized domains such as cryptography, security, and systems programming.

There's potential for integrating ideas from dependent type theory into mainstream programming languages. This could lead to more reliable and secure software development practices.

2. OVERVIEW

Agda:

Dependent Types: Agda allows you to define types that depend on values, making it possible to express complex relationships between data and functions.

Proofs as Programs: In Agda, proofs are written as programs, and programs are verified proofs. This principle, known as the Curry-Howard isomorphism, enables you to write code that is both correct and formally verified.

Interactive Development: Agda provides an interactive development environment where you can define functions, prove theorems, and experiment with different approaches.

Coq:

Coq is French for Rooster. Coq is free, open-source software.

Coq is an interactive theorem prover, development started in 1983 and was first released in 1989.

Implemented in the OCaml programming language.

Reference Manual  https://coq.inria.fr/doc/V8.20.0/refman/

Calculus of Inductive Constructions: Coq is based on a powerful type theory called the Calculus of Inductive Constructions, which allows for higher-order reasoning and the definition of complex mathematical structures.

Tactics: Coq uses tactics to guide the proof process, allowing you to break down complex proofs into smaller, more manageable steps.

Formal Verification: Coq is widely used for formal verification of software and hardware, ensuring that systems are correct by construction.

3. Learning Resources:

Agda:

Official Tutorial:

https://agda.readthedocs.io/en/v2.6.0.1/getting-started/tutorial-list.html

Software Foundations in Agda:

 https://softwarefoundations.cis.upenn.edu/

Type-Driven Development with Idris:

https://www.amazon.com/Type-driven-Development-Idris-Edwin-Brady/dp/1617293024 (While this book is about Idris, it covers many concepts relevant to Agda)

Coq:

Software Foundations: 

The Coq system contains the functional programming language Gallina.

https://softwarefoundations.cis.upenn.edu/

https://www.youtube.com/watch?v=BGg-gxhsV4E&list=PLre5AT9JnKShFK9l9HYzkZugkJSsXioFs

Certified Programming with Coq:

https://www.amazon.com/Certified-Programming-Dependent-Types-Introduction/dp/0262026651

Coq'Art: The Art of Proof and Programming: 

https://link.springer.com/book/10.1007/978-3-662-07964-5

4. Getting Started:

Install: Download and install Agda or Coq for your operating system.

Learn the Basics: Start with the official tutorials or books to understand the syntax and basic concepts.

Practice: Work through exercises and examples to gain practical experience.

Explore Libraries: Use existing libraries to learn from others and build upon their work.

Join the Community: Participate in online forums and communities to ask questions and get help.

Remember, learning Agda and Coq requires patience and persistence. Don't be afraid to experiment and make mistakes. The more you practice, the better you'll become.

3. CONCLUSION

While Agda and Coq may not become mainstream programming languages like Python or JavaScript, their impact on the software development landscape is likely to grow. As the demand for rigorous verification and formal methods increases, these languages have the potential to become indispensable tools for developers and researchers alike.

4. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL DIRECT PROOF

REVISED: Monday, October 28, 2024

1. INTRODUCTION

A Direct Proof is a mathematical method that uses known facts to show the truth or falsehood of a statement. It's a sequence of statements that use definitions, theorems, and logic to prove a conclusion. 

If P then Q or P implies Q is a Direct Proof. For our Direct Proof, we assume P is True and accomplish the proof by using P to prove Q is True. 

An expression of the form P => Q (if P, then Q; Q if P) is called the implication of P and Q. P is the antecedent of the implication and Q the consequent.

If we want to implement implication in Haskell, we can do so in terms of if, then, not, and || or.

The Boolean otherwise is defined as the value True.

The only time an implication is False is when the antecedent P is True and the consequent Q is False.

2. DEFINITIONS (DEF)

DEF 1

An integer 'n' is even if and only if there exists an integer 'k' such that n = 2k

 

DEF 2

An integer 'n' is odd if and only if there exists an integer 'k' such that n = 2k+ 1

DEF 3

Two integers 'a' and 'b' are consecutive if and only if  b = a + 1

3. PROOF 1

Theorem: The sum of any two consecutive integers is odd.

Assume 'a' and 'b' are consecutive integers.

b = a + 1                                                              -- def 3

If 'a' and 'b' are consecutive integers, then by Definition 3, 'b' must be one more than 'a'.

(a + b) = a + (a + 1)                                             -- def 3

(a + b) = 2a + 1                                                    -- def 2

Since 2a is an even integer (by Definition 1), and adding 1 to an even integer always results in an odd integer (by Definition 2), (a + b) is odd.

Q.E.D. “Which was to be demonstrated".  Signifies the end of a proof.

A  □ tombstone symbol is also often used to signify the end of a proof.

4. PROOF 2

While Haskell can be used to represent and reason about mathematical proofs, it's not a direct tool for automating the process of constructing complex proofs. However, we can leverage its type system and functional paradigm to encode simple proofs and reason about them.

A Simple Proof in Haskell: The Sum of Two Even Numbers

Let's consider a simple proof: "The sum of two even numbers is even." We can represent this in Haskell using types and functions:

Theorem: The sum of two even numbers is even.

Haskell

-- Define an even number as a number divisible by 2

data Even = Even Int

-- Define a function to add two even numbers

addEven :: Even -> Even -> Even

addEven (Even x) (Even y) = Even (x + y)

Breakdown:

Data Type Even:

This data type represents an even number. It takes an integer and wraps it in the Even constructor.

Function addEven:

This function takes two Even values and returns an Even value.

It extracts the underlying integers, adds them, and constructs a new Even value.

How Does This Represent a Proof?

Type Safety: The type system ensures that the addEven function can only be applied to two Even values. This guarantees that the input numbers are indeed even.

Functional Purity: Haskell's functional nature ensures that the addEven function always produces the same output for the same input. This eliminates side effects and makes reasoning about the function's behavior straightforward.

Limitations and Advanced Techniques:

While this simple example demonstrates the potential of Haskell for representing and reasoning about mathematical proofs, it's important to note its limitations:

Complex Proofs: For more complex proofs involving multiple steps, quantifiers, and logical connectives, Haskell's type system alone may not be sufficient.

Proof Automation: While Haskell can help formalize and reason about proofs, it doesn't automate the discovery of proofs. Human ingenuity is still required to devise proof strategies.

Advanced Techniques:

Dependent Types: Dependent types allow types to depend on values, enabling more expressive and precise type systems. This can be used to encode more complex mathematical properties.

Proof Assistants: Tools like Agda and Coq are built on top of dependent type theories and provide formal proof systems for verifying mathematical theorems.

5. CONCLUSION

While Haskell is a powerful tool for representing and reasoning about mathematical concepts, it's not a substitute for human mathematical reasoning. However, it can be used to formalize and verify proofs, especially in conjunction with advanced techniques like dependent types and proof assistants.

The goal of a proof is not only to arrive at the correct conclusion but also to present a clear and convincing argument. You want to make your proofs rigorous and easy to understand.

6. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL FUNCTION PROOFS

 

REVISED: Monday, October 28, 2024

1. INTRODUCTION

Haskell Functions as Mathematical Functions

In Haskell, functions are conceptualized as mathematical functions, mapping inputs to outputs. This means they take one or more values as arguments and produce a single result.

Pure Functions

Haskell functions are inherently pure, meaning they have the following properties:

No side effects: They don't modify external state or produce observable effects beyond their return value.

Referential transparency: Replacing a function call with its result doesn't change the program's behavior.

First-Class Citizens

Functions in Haskell are first-class citizens, treated like any other data type:

Passed as arguments: You can pass functions as arguments to other functions.

Returned as values: Functions can return other functions as results.

Assigned to variables: You can store functions in variables.

Syntax and Types

Definition: Functions are defined using the = operator.

Type annotation: The type of a function is specified after its name, using ::. For example, f :: Int -> Int indicates that f takes an integer as input and returns an integer.

Arguments: Multiple arguments are separated by spaces.

Return value: The return value is the expression on the right side of the = operator.

Examples

Simple function:

add :: Num a => a -> a -> a

add x y = x + y

Function taking multiple arguments:

multiply :: Num a => a -> a -> a -> a

multiply x y z = x * y * z

Function returning a function:

makeAdder :: Num a => a -> a -> a

makeAdder x = (\y -> x + y)

Higher-Order Functions

Haskell supports higher-order functions, taking functions as arguments or returning functions as results. This enables powerful programming techniques like:

Map: Applies a function to each element of a list.

map :: (a -> b) -> [a] -> [b]

Filter: Selects elements from a list based on a predicate function.

filter :: (a -> Bool) -> [a] -> [a]

Reduce: Combines elements of a list using a binary function.

reduce :: Integral a => a -> a -> Ratio a

Recursion

Recursion is a common programming technique in Haskell, where a function calls itself to solve smaller instances of a problem. Haskell's type system and pattern matching make it well-suited for recursive functions.

Benefits of Haskell Functions

Readability: Haskell's functional style and concise syntax make code more readable and easier to understand.

Correctness: Pure functions are easier to reason about and test for correctness.

Concurrency: Haskell's functional nature makes it well-suited for concurrent programming.

Modularity: Functions can be composed to build complex programs from smaller, reusable components.

By understanding these concepts, you can effectively use Haskell functions to write elegant, efficient, and maintainable code.

2. PROOFS

Computer program function proofs are mathematical proofs partially or fully generated by a computer program.

You can evaluate (prove) Integer arithmetic; however, computers still have problems with Floating-Point arithmetic. 

Before assuming a Lemma check it with QuickCheck. 

A function algorithm proof is a step-by-step procedure or formula for calculations, problem-solving operations, or accomplishing a task in a certain number of steps.

There are four basic proof techniques used in mathematics: Direct Proof, Proof by Contradiction, Proof by Induction, and Proof by Contrapositive.

PROOF BY INDUCTION EXAMPLE

Proving a recursion reverse function:

sum (reverse [])       = sum []                                               -- def reverse base case

sum (reverse (x:xs)) = sum (reverse xs ++ [x])                  -- def reverse recursion

Base Case:

sum (reverse []) = sum []

This follows directly from the definition of reverse and sum.

Recursive Case:

Inductive Hypothesis: Assume that sum (reverse ys) = sum ys for all lists ys.

Inductive Steps:

sum (reverse (x:xs)) = sum (reverse xs ++ [x])       -- definition of `reverse`

sum (reverse (x:xs)) = sum (reverse xs) + sum [x]  -- lemma (proven below separately)

sum (reverse (x:xs)) = sum xs + sum [x]                  -- inductive hypothesis

sum (reverse (x:xs)) = sum xs + x                             -- definition of `sum`

sum (reverse (x:xs)) = sum (x:xs)                             -- definition of `sum`

Key Points:

The proof relies on a strong inductive hypothesis and a correctly proven lemma.

The commutativity of sum is implicitly used, a direct consequence of the definition.

A formal proof of the lemma enhances the rigor of the overall proof.

LEMMA PROOF

The lemma can be proven using the definition of sum and induction on the length of xs.

Proving the Lemma: sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]

Proof by Induction on the Length of xs:

Base Case:

When xs = []:

sum (reverse [] ++ [x]) = sum ([x]) = x

sum (reverse []) + sum [x] = sum [] + sum [x] = 0 + x = x

Thus, the equation holds for the base case.

Recursive Case:

Inductive Hypothesis: Assume the equation holds for a list xs of length n. That is:

sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]

Inductive Steps:

Consider a list (y:xs) of length n+1:

sum (reverse (y:xs) ++ [x])

= sum (reverse xs ++ [y] ++ [x])          -- Definition of `reverse`

= sum (reverse xs ++ [y + x])               -- Definition of `++` and `sum`

= sum (reverse xs) + sum [y + x]          -- Inductive Hypothesis

= sum (reverse xs) + (y + x)                   -- Definition of `sum`

= (sum (reverse xs) + y) + x                   -- Associativity of `+`

= (sum (reverse xs) + sum [y]) + x         -- Definition of `sum`

= sum (reverse xs) + (sum [y] + x)         -- Associativity of `+`

= sum (reverse xs) + sum [y, x]               -- Definition of `sum` and `++`

= sum (reverse xs) + sum [x, y]               -- Commutativity of `+`

= sum (reverse xs) + sum [x] + sum [y]  -- Definition of `sum`

= sum (reverse xs) + sum [x]                    -- Definition of `sum` for a singleton list

Therefore, by the principle of mathematical induction, the lemma holds for all lists xs.

3. CONCLUSION

The concept of pure functionality in Haskell makes its code easier to prove correct than imperative languages.

4. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.

HASKELL LOGARITHMS

REVISED: Sunday, October 13, 2024

1. INTRODUCTION

As mentioned in previous tutorials, Haskell has three exponentiation operators: (^), (^^), and (**). ^ is non-negative integral exponentiation, ^^ is integer exponentiation, and ** is floating-point exponentiation.

Use the ^ exponent operator when you need a non-negative integer as the exponent.

Prelude>  2 ^ 5

32

it :: Num a => a

Prelude>

Prelude>  :type (^)

(^) :: (Num a, Integral b) => a -> b -> a

Prelude>

Prelude>  :info (^)

(^) :: (Num a, Integral b) => a -> b -> a -- Defined in `GHC.Real'

infixr 8 ^

Prelude>    

Prelude>  2 ^ (-5)

*** Exception: Negative exponent

Prelude>

Use the ^^ exponent operator when you need a positive or negative integer as the exponent.

Prelude>  2 ^^ 5

32.0

Prelude>

Prelude>  :type (^^)

(^^) :: (Integral b, Fractional a) => a -> b -> a

Prelude>  

Prelude>  :info (^^)

(^^) :: (Fractional a, Integral b) => a -> b -> a

  -- Defined in ‘GHC.Real’

infixr 8 ^^

Prelude>  

Prelude>  2 ^^ (-5)

3.125e-2

Prelude>

Use the ** exponent operator when you need a positive or negative floating point number as the exponent.

Prelude> 2 ** 5.0

32.0

it :: Floating a => a

Prelude> 

Prelude>  :type (**)
(**) :: Floating a => a -> a -> a

Prelude>

Prelude>  :info (**)

class Fractional a => Floating a where

  ...
  (**) :: a -> a -> a
  ...
         -- Defined in `GHC.Float'
infixr 8 **
Prelude>  

Prelude>  2 ** (-5.0)

3.125e-2

Prelude>

Use the exp exponent operator to use Euler's number e,  the base of the Natural Logarithms.

Logarithms are another way of thinking about exponents. For example, in exponential form 2 ³ = 8, and in logarithmic form log ₂ 8 = 3. In other words, if b ^x  = y, log _b y = x where the base is b and the exponent is x.

Furthermore:

log _b (xy) = log _b x + log _b y

log _b (x/y) = log _b x - log _b y

log _b (x ^y) = y (log _b x)

Prelude>  exp 1

2.718281828459045

it :: Floating a => a

Prelude> 

Prelude>  :type exp

exp :: Floating a => a -> a

Prelude>

Prelude>  :info exp

class Fractional a => Floating a where

  ...

  exp :: a -> a

  ...

  -- Defined in `GHC.Float'

Prelude>  

Prelude>  let e = exp 1
e :: Floating a => a

Prelude>

= denotes definition, like it does in mathematics; e.g., e "is defined as" exp 1.

Prelude>  e
2.718281828459045
it :: Floating a => a

Prelude>

Haskell provides various approaches to solving logarithmic equations, depending on the complexity and desired accuracy.

2. OVERVIEW

 

The following are three common methods which can be used to solve logarithmic equations.

2.1. Using Logarithmic Properties:

This method exploits the logarithmic properties, such as product rule, quotient rule, and power rule, to manipulate the equation into a form where the unknown variable can be isolated.

2.2. Using Numerical Methods:

For more complex equations or when analytical solutions are difficult, numerical methods like bisection method or Newton-Raphson method can be applied. These methods iteratively refine an initial guess until the desired accuracy is reached.

2.3. Using Symbolic Libraries:

Libraries like "symbolic" or "polyglot" allow symbolic manipulation of expressions, enabling you to solve equations for exact solutions without numerical approximations.

3. EXAMPLES

3.1. Using Logarithmic Properties:

--  logProp.hs

import Prelude hiding ((**))

-- Function to apply a logarithmic property

applyProperty :: (Double -> Double) -> Double -> Double -> Double

applyProperty f x y = f (x * y)

-- Example equation: 3^x = 81

solveEquation :: Double -> Double

solveEquation x =

  let

    leftSide = exp (x * logBase 10 3)  -- Apply power rule

    rightSide = 81

  in

    logBase 10 rightSide / logBase 10 3  -- Apply quotient rule

main :: IO ()

main = do

  let solution = solveEquation 1.0  -- Starting with a guess of 1.0

  print solution

 

Windows PowerShell

Copyright (C) Microsoft Corporation. All rights reserved.

PS C:\Users\User> ghci

GHCi, version 9.4.8: https://www.haskell.org/ghc/  :? for help

ghci> :cd C:\Users\User\tinnel\Haskell 2024\newProjects

ghci> :l logProp.hs

[1 of 2] Compiling Main             ( logProp.hs, interpreted )

Ok, one module loaded.

ghci> main

4.0

ghci>

Explanation:

Import Prelude: This module provides basic functions and types, including logBase and exp for logarithms and exponents.

applyProperty: This function demonstrates applying a logarithmic property to two numbers. It's not used directly in this example, but it illustrates the concept.

solveEquation: Takes a guess for x as input. Calculates the left side of the equation using exp (x * logBase 10 3), applying the power rule of logarithms. Compares the left side to the right side (81). Applies the quotient rule of logarithms to isolate x and return its value.

main: Calls solveEquation with an initial guess of 1.0. Prints the solution, which should be 4.0 (since 3^4 = 81).

Key Points:

The program uses logBase 10 for base-10 logarithms. You can use a log for natural logarithms (base e).

It assumes a simple equation with known values, but this approach can be applied to more complex equations as well.

You should use numerical methods to solve equations or find roots in more sophisticated cases. 

3.2. Using the Bisection Method:

-- bisecMeth.hs

import Prelude hiding ((**))

-- Function representing the logarithmic equation

eqn :: Double -> Double

eqn x = log x - 2  -- Example: log(x) = 2

-- Bisection method

bisection :: Double -> Double -> Double -> Double -> Double

bisection a b tolerance iterations =

  let mid = (a + b) / 2

      fmid = eqn mid

      error = abs (b - a)

  in

    if error < tolerance || iterations == 0

      then mid

      else if fmid * eqn a < 0

          then bisection a mid tolerance (iterations - 1)

          else bisection mid b tolerance (iterations - 1)

main :: IO ()

main = do

  let solution = bisection 1.0 10.0 1e-6 100  -- Initial interval, tolerance, max iterations

  print solution

Windows PowerShell

Copyright (C) Microsoft Corporation. All rights reserved.

PS C:\Users\User> ghci

GHCi, version 9.4.8: https://www.haskell.org/ghc/  :? for help

ghci> :cd C:\Users\User\tinnel\Haskell 2024\newProjects

ghci> :l bisecMeth.hs

[1 of 2] Compiling Main             ( bisecMeth.hs, interpreted )

Ok, one module loaded.

ghci> main

7.38905593752861

ghci>

Explanation:

Import Prelude: Provides basic functions and types, including log for logarithms.

eqn: Represents the logarithmic equation to be solved.

bisection: Implements the bisection algorithm: Takes the initial interval (a, b), tolerance, and maximum iterations as input. Recursively halves the interval based on the sign of fmid * eqn a. Checks for convergence based on error or maximum iterations.

main: Calls bisection with an initial interval of (1.0, 10.0), tolerance of 1e-6, and maximum iterations of 100. Prints the solution, which should be approximately 7.389065 (since log(7.389065) ≈ 2).

Key Points:

The bisection method is generally more robust than the Newton-Raphson method, as it doesn't require calculating a derivative and can handle a wider range of equations. It converges slower than Newton-Raphson but is guaranteed to converge if the equation has a root within the initial interval. You can adjust the initial interval, tolerance, and maximum iterations to suit your specific problem.

3.3. Newton-Raphson Method:

-- newRap.hs

import Prelude hiding ((**))

-- Function representing the logarithmic equation

eqn :: Double -> Double

eqn x = log x - 2  -- Example: log(x) = 2

-- Derivative of the equation

eqnDeriv :: Double -> Double

eqnDeriv x = 1 / x

-- Newton-Raphson method

newtonRaphson :: Double -> Double -> Double -> Double

newtonRaphson x0 tolerance iterations =

  let x1 = x0 - eqn x0 / eqnDeriv x0

      error = abs (x1 - x0)

  in

    if error < tolerance || iterations == 0

      then x1

      else newtonRaphson x1 tolerance (iterations - 1)

main :: IO ()

main = do

  let solution = newtonRaphson 1.0 1e-6 100  -- Initial guess, tolerance, max iterations

  print solution

PS C:\Users\User> ghci

GHCi, version 9.4.8: https://www.haskell.org/ghc/  :? for help

ghci> :cd C:\Users\User\tinnel\Haskell 2024\newProjects

ghci> :l newRap.hs

[1 of 2] Compiling Main             ( newRap.hs, interpreted )

Ok, one module loaded.

ghci> main

7.389056098930626

ghci>

Explanation:

Import Prelude: Provides basic functions and types, including log for logarithms.

eqn: Represents the logarithmic equation to be solved.

eqnDeriv: Calculates the derivative of the equation, needed for the Newton-Raphson method.

newtonRaphson: Implements the Newton-Raphson algorithm: Takes the initial guess, tolerance, and maximum iterations as input. Recursively updates the guess using the formula x1 = x0 - eqn x0 / eqnDeriv x0. Checks for convergence based on error or maximum iterations.

main: Calls newtonRaphson with an initial guess of 1.0, tolerance of 1e-6, and maximum iterations of 100. Prints the solution, which should be approximately 7.389056 (since log(7.389056) ≈ 2).

Key Points:

You can adjust the equation (eqn), derivative (eqnDeriv), tolerance, and maximum iterations to solve different logarithmic equations.

The method might not converge for all equations or initial guesses.

Other numerical methods, like the bisection method, can also be implemented in Haskell using similar techniques.

3.4. Symbolic Libraries:

While Haskell doesn't have a library named "symbolic" specifically for symbolic computation, it does have several libraries that offer symbolic capabilities:

3.4.1. SBV (Satisfiability Modulo Theories):

Provides symbolic reasoning for expressions and constraints. Can be used to solve equations, prove theorems, and model systems.

-- satModTh.hs

-- The Data.SBV module is not part of the standard Haskell libraries and can not currently be imported. However, the following program is shown and can be used when its import is available.

import Data.SBV

solveEquation :: SymExpr Solver -> IO ()

solveEquation expr = do

    model <- getModel expr

    print (eval model expr)

main :: IO ()

main = do

    let x = free "x" :: SymExpr Solver

    solveEquation (log x .== 2)

3.4.2. Grisette:

Offers symbolic evaluation of Haskell expressions. Useful for constraint solving, testing, and analysis.

-- grisette.hs

-- Data.Grisette.Crucible.Core can not currently be imported; however, the following program is shown and can be used when its import is available.

import Data.Grisette.Crucible.Core

solveEquation :: Expr -> IO ()

solveEquation expr = do

    result <- evaluate expr

    print result

main :: IO ()

main = do

    let x = mkVar "x" :: Expr

    solveEquation (log x .== 2)

3.4.3. Polyglot:

A frontend for various symbolic backends (e.g., Mathematica, SymPy).  Allows interaction with these systems from Haskell.

-- polyglot.hs

-- Language.Polyglot can not currently be imported; however, the following program is shown and can be used when its import is available.

import Language.Polyglot

solveEquation :: String -> IO ()

solveEquation expr = do

    result <- runSession $ runMathematica $ expr

    print result

main :: IO ()

main = do

    solveEquation "Solve[Log[x] == 2, x]"

Choosing the right library depends on your specific requirements and the complexity of the symbolic tasks you need to perform.

4. CONCLUSION

Choose the method based on the equation's complexity and desired accuracy.

Numerical methods may require fine-tuning initial guess and tolerance parameters.

Symbolic libraries offer exact solutions but might not be efficient for all cases.

5. REFERENCES

Bird, R. (2015). Thinking Functionally with Haskell. Cambridge, England: Cambridge University Press.

Davie, A. (1992). Introduction to Functional Programming Systems Using Haskell. Cambridge, England: Cambridge University Press.

Goerzen, J. & O'Sullivan, B. &  Stewart, D. (2008). Real World Haskell. Sebastopol, CA: O'Reilly Media, Inc.

Hutton, G. (2007). Programming in Haskell. New York: Cambridge University Press.

Lipovača, M. (2011). Learn You a Haskell for Great Good!: A Beginner's Guide. San Francisco, CA: No Starch Press, Inc.

Thompson, S. (2011). The Craft of Functional Programming. Edinburgh Gate, Harlow, England: Pearson Education Limited.