Add transformation to applicative terms and enhance the UI

Author: nigosto

README.md

@@ -1,13 +1,16 @@
 # lambda-parser
-Parser for lambda terms, written in Haskell, that is also able to apply substitution, according to the rules of lambda calculus
+Parser for lambda terms, written in Haskell, that is also able to execute a list of operations on the terms
 
 ## Table of contents
 - [Prerequisites](#prerequisites)
 - [Running the project](#running-the-project)
 - [Installing the executable manually](#installing-the-executable-manually)
 - [Documentation](#documentation)
     - [Grammar](#grammar)
-    - [Substitution](#substitution)
+    - [Supported operations](#supported-operations)
+        - [Substitution](#substitution)
+        - [Transformation to applicative term](#transformation-to-applicative-term)
+        - [Counting beta-redexes](#counting-beta-redexes)
 - [License](#license)
 - [Contacts](#contacts)
 
@@ -35,7 +38,7 @@ cabal install
 Now the executable should be located in the configured `installdir` of `cabal` (usually `~/.local/bin` or `~/.cabal/bin`).
 
 ## Documentation
-The parser traverses the lambda term and creates AST where the nodes are variables, applications and abstractions (lexing and parsing are done simultaneously). Then the substitution is done on the AST with the corresponding tokens instead of directly on the term. After the substitution, a new lambda term is generated based on the newly created AST and the result is returned as the final answer. If there are no brackets, the application term is left associative. Bear in mind that in the generated final term some brackets may be added because there is no way to know where they can be skipped without looking ahead, which the current generator does not do.
+The parser traverses the lambda term and creates AST where the nodes are variables, applications and abstractions (lexing and parsing are done simultaneously). Then the operations are done on the AST with the corresponding tokens instead of directly on the term. After the operation, a new lambda term is generated based on the newly created AST and the result is returned as the final answer. If there are no brackets, the application term is left associative. Bear in mind that in the generated final term some brackets may be added because there is no way to know where they can be skipped without looking ahead, which the current generator does not do.
 
 ### Grammar
 $` variable \Coloneqq [a-z] `$ <br>
@@ -45,11 +48,20 @@ $`   \quad \quad \quad \quad \ \ | \quad λ \ \langle variable\rangle \ . \ \lan
 
 (Here $` (\!( \ )\!)^* `$ means that the brackets themselves are optional)
 
-### Substitution
+### Supported operations
+This is the list of currently supported operations, that can be executed on the terms after parsing:
+
+#### Substitution
 There are currently 2 supported versions for the substitutions:
 - curry substitution - this is the standart substitution, done directly on the original term. In order for it to be correct and not change the semantics of the lambda terms, in the cases where a naive substitution would cause a problem, the bound variables are renamed. The algorithm starts by trying all letters, starting from *a*, until a letter is found that would not cause the term to change its semantics and renames the bound variable with the found letter. If a suitable letter is not found, then the algorithm continues to search for any suitable character (which does not follow the grammar);
 - nameless term substitution - in order for this substitution to be applied the term is first transformed into nameless term. Nameless terms don't have variable names - instead de Bruijn indexes are used to denote which variables are bound and which - free. The substitution is then done on the indexes instead of the variables by utilizing the `shift` function. After the substitution is done, the term is transformed back into its named version, where the bound variables may have different names (which does not change the semantics of the term).
 
+#### Transformation to applicative term 
+The transformation to applicative term is non-deterministic operation because there are 2 approaches to it - either to start from the outside or the inside. The algorithm always starts from the outside, except in the case where starting from the outside would not lead to the full transformation - this is the case where there are 2 nested abstractions where the argument of the first is part of the free variables of the second. When this case is encountered the transformation is applied to the inner abstraction first and after it is done the partial result is transformed again to achieve the coorect result.
+
+#### Counting beta-redexes
+Counting the beta-redexes in s single term is the simplest operation. The algorithm traverses the AST and counts the occurences of applications where the first argument is abstraction.
+
 ## License
 The project is licensed under the MIT License. See the [LICENSE](./LICENSE) file for more information.
 

lambda-parser.cabal

@@ -31,12 +31,14 @@ executable lambda-parser
         Examples.Terms
         Interaction
         Parser
-        Transformer
-        Generator
+        Transformers
+        Generators
         Substitution.Named
         Substitution.Nameless
         Libs.Stack
         Libs.BetaRedexes
+        Utils.Variables
+        Terms
 
     -- LANGUAGE extensions used by modules in this package.
     -- other-extensions:

src/Generator.hs

@@ -0,0 +1,46 @@
+module Generators where
+
+import Terms (Term (..), ApplicativeTerm (..), Combinator (..), NamelessTerm (..))
+
+generateTerm :: Term -> String
+generateTerm (Variable var) = [var]
+generateTerm (Application lhs rhs) =
+  let generatedLhs = case lhs of
+        var@(Variable _) -> generateTerm var
+        application@(Application _ _) -> generateTerm application
+        abstraction@(Abstraction _ _) -> '(' : generateTerm abstraction ++ [')']
+      generatedRhs = case rhs of
+        var@(Variable _) -> generateTerm var
+        application@(Application _ _) -> '(' : generateTerm application ++ [')']
+        abstraction@(Abstraction _ _) -> '(' : generateTerm abstraction ++ [')']
+   in generatedLhs ++ generatedRhs
+generateTerm (Abstraction argument body) = 'λ' : argument : '.' : generateTerm body
+
+generateNamelessTerm :: NamelessTerm -> String
+generateNamelessTerm (NamelessVariable var) = show var
+generateNamelessTerm (NamelessApplication lhs rhs) =
+  let generatedLhs = case lhs of
+        var@(NamelessVariable _) -> generateNamelessTerm var
+        application@(NamelessApplication _ _) -> generateNamelessTerm application
+        abstraction@(NamelessAbstraction _) -> '(' : generateNamelessTerm abstraction ++ [')']
+      generatedRhs = case rhs of
+        var@(NamelessVariable _) -> generateNamelessTerm var
+        application@(NamelessApplication _ _) -> '(' : generateNamelessTerm application ++ [')']
+        abstraction@(NamelessAbstraction _) -> '(' : generateNamelessTerm abstraction ++ [')']
+   in generatedLhs ++ generatedRhs
+generateNamelessTerm (NamelessAbstraction body) = 'λ' : generateNamelessTerm body
+
+generateCombinator :: Combinator -> String
+generateCombinator KCombinator = "K"
+generateCombinator SCombinator = "S"
+
+generateApplicativeTerm :: ApplicativeTerm -> String
+generateApplicativeTerm (ApplicativeVariable var) = [var]
+generateApplicativeTerm (ApplicativeApplication lhs rhs) =
+  let generatedLhs = generateApplicativeTerm lhs
+      generatedRhs = case rhs of
+        var@(ApplicativeVariable _) -> generateApplicativeTerm var
+        application@(ApplicativeApplication _ _) -> '(' : generateApplicativeTerm application ++ [')']
+        combinator@(ApplicativeCombinator _) -> generateApplicativeTerm combinator
+   in generatedLhs ++ generatedRhs
+generateApplicativeTerm (ApplicativeCombinator combinator) = generateCombinator combinator

src/Generators.hs

@@ -1,13 +1,21 @@
 module Interaction where
 
 import Prelude hiding (lookup)
-import Generator (generateTerm, generateNamelessTerm)
+import Generators (generateTerm, generateNamelessTerm, generateApplicativeTerm)
 import Parser (parseTerm)
 import Libs.Stack (emptyStack)
 import Substitution.Named (substitute)
-import Transformer (toNameless, toNamed)
+import Transformers (toNameless, toNamed, toApplicative)
 import Data.Map (empty, lookup)
 import Substitution.Nameless (substituteNameless)
+import Libs.BetaRedexes (extractBetaRedexes)
+
+requestMode :: IO Int
+requestMode = do
+  putStrLn "Please choose what kind of operation you want to do (1, 2, 3):"
+  putStrLn "1) Substitution"
+  putStrLn "2) Transformation from λ-term to Applicative term"
+  putStrLn "3) Count beta-redexes in λ-term" >> read <$> getLine
 
 data TermType = Nameless | Named deriving (Show, Eq)
 
@@ -39,3 +47,26 @@ doSubstituteNameless term var substituteTerm outputTermType =
        in if outputTermType == Named 
           then generateTerm $ toNamed result updatedContext
           else generateNamelessTerm result
+
+executeSubstitution :: IO ()
+executeSubstitution = do
+  term <- putStr "Input term: " >> getLine
+  var <- putStr "Input variable to substitute: " >> getLine -- not using getChr intentionally
+  if length var /= 1
+    then error "please provide valid variable"
+    else do
+      substituteTerm <- putStr "Input substitution term: " >> getLine
+      substitutionType <- getSubstitutionType
+      if substitutionType == Named
+      then putStrLn $ doSubstituteNamed term var substituteTerm
+      else do
+        outputFormat <- getOutputTermType
+        putStrLn $ doSubstituteNameless term var substituteTerm outputFormat
+
+executeTransformationToApplicative :: IO ()
+executeTransformationToApplicative =
+  putStr "Input term: " >> flip parseTerm emptyStack <$> getLine >>= putStrLn . generateApplicativeTerm . toApplicative
+
+executeBetaRedexesCount :: IO ()
+executeBetaRedexesCount =
+  putStr "Input term: " >> flip parseTerm emptyStack <$> getLine >>= mapM_ (putStrLn . generateTerm) . extractBetaRedexes

src/Interaction.hs

@@ -1,15 +1,11 @@
 module Libs.BetaRedexes where
-import Parser (Term (Variable, Application, Abstraction))
-import Generator (generateTerm)
+import Terms (Term (..))
+import Generators (generateTerm)
 
 extractBetaRedexes :: Term -> [Term]
 extractBetaRedexes (Variable _) = []
 extractBetaRedexes term@(Application lhs@(Abstraction _ body) rhs) =
   term : extractBetaRedexes body ++ extractBetaRedexes rhs
 extractBetaRedexes (Application lhs rhs) =
   extractBetaRedexes lhs ++ extractBetaRedexes rhs
-extractBetaRedexes (Abstraction _ body) = extractBetaRedexes body
-
-displayBetaRedexes :: Term -> IO ()
-displayBetaRedexes term =
-  mapM_ (putStrLn . generateTerm) $ extractBetaRedexes term
+extractBetaRedexes (Abstraction _ body) = extractBetaRedexes body

src/Libs/BetaRedexes.hs

@@ -1,20 +1,18 @@
 module Main where
 
 import System.IO (BufferMode (BlockBuffering), hSetBuffering, stdout)
-import Interaction (getSubstitutionType, getOutputTermType, doSubstituteNameless, TermType (Named), doSubstituteNamed)
+import Interaction (
+  requestMode, 
+  executeSubstitution,
+  executeTransformationToApplicative, 
+  executeBetaRedexesCount)
 
 main :: IO ()
 main = do
   hSetBuffering stdout $ BlockBuffering $ Just 1
-  term <- putStr "Input term: " >> getLine
-  var <- putStr "Input variable to substitute: " >> getLine -- not using getChr intentionally
-  if length var /= 1
-    then error "please provide valid variable"
-    else do
-      substituteTerm <- putStr "Input substitution term: " >> getLine
-      substitutionType <- getSubstitutionType
-      if substitutionType == Named
-      then putStrLn $ doSubstituteNamed term var substituteTerm
-      else do
-        outputFormat <- getOutputTermType
-        putStrLn $ doSubstituteNameless term var substituteTerm outputFormat
+  modeIndex <- requestMode
+  case modeIndex of
+    1 -> executeSubstitution
+    2 -> executeTransformationToApplicative
+    3 -> executeBetaRedexesCount
+    _ -> putStrLn "Unrecognized operation!" >> main

src/Main.hs

@@ -1,13 +1,8 @@
-module Parser (parseTerm, Term(Variable, Application, Abstraction)) where
+module Parser (parseTerm) where
 
 import Data.Char (isAlpha)
 import Libs.Stack (Stack, peek, pop, emptyStack, push)
-
-data Term =
-  Variable Char |
-  Application Term Term |
-  Abstraction Char Term
-  deriving (Show)
+import Terms (Term (..))
 
 takeWhileClosingBracket :: String -> Int-> String
 takeWhileClosingBracket ('(':xs) count = '(':takeWhileClosingBracket xs (count + 1)

src/Parser.hs

@@ -1,12 +1,8 @@
 module Substitution.Named where
 
-import Parser (Term (Application, Variable, Abstraction))
+import Terms (Term (Application, Variable, Abstraction))
 import Data.Char (chr, ord)
-
-freeVariables :: Term -> [Char]
-freeVariables (Variable x) = [x]
-freeVariables (Application lhs rhs) = freeVariables lhs ++ freeVariables rhs
-freeVariables (Abstraction argument body) = filter (/= argument) $ freeVariables body
+import Utils.Variables (freeVariables)
 
 chooseUniqueVariable :: Term -> Term -> Char
 chooseUniqueVariable first second = let vars = freeVariables first ++ freeVariables second

src/Substitution/Named.hs

@@ -1,5 +1,5 @@
 module Substitution.Nameless where
-import Transformer (NamelessTerm (NamelessVariable, NamelessApplication, NamelessAbstraction), NamingContext)
+import Terms (NamelessTerm (..))
 
 shift :: Int -> Int -> NamelessTerm -> NamelessTerm
 shift c d var@(NamelessVariable k)

src/Substitution/Nameless.hs

@@ -0,0 +1,21 @@
+module Terms where
+
+data Term =
+  Variable Char |
+  Application Term Term |
+  Abstraction Char Term
+  deriving (Show, Eq)
+
+data NamelessTerm
+  = NamelessVariable Int
+  | NamelessApplication NamelessTerm NamelessTerm
+  | NamelessAbstraction NamelessTerm
+  deriving (Show)
+
+data Combinator = KCombinator | SCombinator deriving (Eq)
+
+data ApplicativeTerm
+  = ApplicativeVariable Char
+  | ApplicativeApplication ApplicativeTerm ApplicativeTerm
+  | ApplicativeCombinator Combinator
+  deriving (Eq)