반응형

항목 9 : typedef 보다는 별칭(using) 을 선호하라.

 

 

STL 컨테이너들을 사용하는 것이 바람직하다. 이건 아마 c++을 사용하는 사람들은 동의 하리라 생각합니다.

std::unique_ptr의 사용 역시 바람직하다는 점에 대해서도 동의 할것 같구요.(저도 동의합니다.)

 

하지만, "std::unique_ptr<unordered_map<std::string, std::string>>" 을 여러번 타이핑하는 것은 하고 싶지 않죠( 120% 공감)

 

이럴때 typedef 를 사용합니다.

typedef std::unique_ptr<unordered_map<std::string, std::string>> UPtrMapSS;

 

C++98 에서 사용하던 방식이죠.

 

C++11에서는 별칭선언(alias declaration) 을 제공합니다.

 

using UPtrMapSSstd::unique_ptr<unordered_map<std::string, std::string>>;

 

 

이 둘의 차이가 있을까요?

 

그전에 한가지!!! (사실 이것 하나만 보더라도 흥미롭습니다.)

 

typedef void(*FP)(int , const std::string&);

 

using FP = void (*)(int, const std::string&);

 

둘 모두 같은 의미입니다. 함수 포인터를 type으로 선언한것인데요.

눈으로 보기에는 using으로 선언한 것이 더 편하고 명확해 보입니다.(물론 함수포인터 선언에 한해서만 봤을때죠.)

 

 

본격적으로 using을 선호해야 하는 이유에 대해서 다룹니다.

 

첫번째 typedef는 template 화 할 수 없습니다. using은 template화 할수 있습니다.

 

template<typename T>

using MyAllocList = std::list<T, MyAlloc<T>>;

MyAllocList<Widget> wg;

 

 

 

typedef를 사용할 경우,

 

template<typename T>

struct MyAllocList {

  typename std::list<T, MyAlloc<T>> type;

};

 

MyAllocList<Widget>::type wg;

 

 

이를 활용하는 template class를 만든다고 합시다.

 

template <typename T>

class Widget {

 private:

   typename MyAllocList<T>::type list;

};

 

C++의 규칙중에는 의존적인 형식(dependent type)의 이름 앞에 반드시 typename을 붙여야 합니다.

 

MyAllocList<T>::type은 템플릿 형식 매개변수 T에 의존적인 형식입니다.

따라서 typename을 붙여야 하며, 또 ::type역시 꼭 필요합니다.

 

보다시피 typedef를 사용하였을때 만들어야 하는 코드를 보면 "어떻게든 되게 만드는" 코드 처럼 보입니다.

 

using은 이런 점들을 보완해서 template을 좀더 자연스럽게 사용할 수 있도록 제공합니다.

template<typename T>

using MyAllocList = std::list<T, MyAlloc<T>>;

template <typename T>

class Widget{

 private:

  MyAllocList<T> list;

}

 

그리고 다음 사항까지도 고려해야합니다.

이 경우 MyAllocList<T>::type은 데이타 타입이 아니라 변수 type이 됩니다.

따라서 반드시 typename을 사용해야 합니다.

 

 

더보기

<검토 필요>

class Wine {...};

 

template <>

class MyAllocList<Wine> {

private:

  enum class WineType {Red, White, Rose};

  WinType type;

};

 

이 경우에  Wine 으로 생성하게 되면 WinType 의 type을 지칭하는 것이 된다.

 

템플릿 메타 프로그래밍은 결국 현재까지 개발된 코드에서 문제 없는가도 중요하지만,

앞으로 개발될 새로운 코드에서도 적용 가능한가도 매우 중요하죠..

 
그때문에 이런 내용들까지도 고려를 해야합니다.

 

 

 

여기서 잠깐, 또 한가지 주의점이 있습니다.

C++11의 STL 에 type과 관련된 template method들이 있습니다.

std::remove_const<T>::type   // const T를 T로 변환

std::remove_reference<T>::type // T& T&&에서 &를 제거

std::add_lvalue_ref<T>::type //T를 T&로 변환

 

이 method들의 구현이 typedef로 구현되어 있기 때문에, ::type이라는 접미사를 붙여야 합니다.

 

이로 인해서 type이라는 이름을 template에서 사용할때는 유의해야합니다.

 

C++14에서는 이를 보완한 멋진 template method들이 있습니다.

 

std::remove_const<T>::type   //C++11

std::remove_const_t<T>      //C++14 에 추가

std::remove_reference<T>::type //C++11

std::remove_reference_t<T>     //C++14에 추가

std::add_lvalue_ref<T>::type //C++11

std::add_lvalue_ref_t<T>     //C++14에 추가

 

아, 그럼 C++11 사용자는 못쓰는건가????

책에 나온 내용을 보면, C++11 컴파일러를 사용하는 사람도 걱정을 할 필요가 없겠더군요.

 

지금까지 살펴본 using을 이용하면 아주 쉽게 처리할 수 있습니다.

 

template <class T>

using remove_const_tstd::remove_const<T>::type;

 

template <class T>

using remove_reference_t = std::remove_reference<T>::type;

 

template <class T>

using add_lvalue_ref_t = std::add_lvalue_ref<T>::type;

 

 

 

[참고] effective modern c++ : 항목 9

 

반응형

noexcept 에 대한 내용입니다.


effective modern c++ 에서 이와 관련된 내용을 다루고 있는데요.

간략한 요약및 꼭 숙지해둘 만한 내용을 적어봤습니다.


항목 14: 예외를 방출하지 않을 함수는 noexcept로 선언하라


exception 은 c++ 98에서 추가되었던 내용입니다. 하지만, 이는 득보다 실이 크다는 것을 많은 C++ 개발자들이 경험했을 것입니다.

함수 구현과 예외 명세, 클라이언트 코드 사이의 일관성 유지에 아무런 도움이 안되었죠.


c++ 11에서는 noexcept라는 키워드를 통해서 클라이언트에게 예외처리가 필요한지 아닌지에 대한 매우 중요한 정보를 전달 할 수 있게 되었습니다.

interface 설계시 매우 중요한 역할을 합니다.


물론 c++98 에서도 throw() 로도 이런 역할을 충분히 할 수 있었습니다.


int f(int x) throw();   //f는 예외를 던지지 않음 : C++98 방식

int f(int x) noexcept; // f는 예외를 던지지 않음 : C++11 방식


throw() 의 경우에는 f가 불린 지점까지의 callstack이 풀리게 됩니다. 그리고 나서 뭔가 처리를 하고 종료(terminate)됩니다.

noexcept의 경우에는 호출 스택이 풀릴 수도 있고 그렇지 않을 수도 있습니다.(좀더 자료 조사가 필요한 부분이네요.)


이런 특성때문에 noexcept로 선언하여 사용하는 경우가 throw()를 사용하는 경우보다 최적화 여지가 더 크다고 합니다.



또 하나의 가장 중요한 기억해야 할 점은,


C++11에서는 기본적으로 모든 메모리 해제 함수와 모든 소멸자 함수는 암묵적으로 noexcept입니다. 따라서 noexcept를 직접 선언할 필요가 없습니다.

만약 소멸자에서 예외를 던지고 싶다면, noexcept(false)로 명시적으로 예외를 발생 시키겠다고 선언한 경우 뿐입니다.


하지만, 기본적으로 C++98이든 C++11이든 소멸자에서 예외를 던지는 것은 나쁜 코딩 습관으로 간주합니다. 

이런 코딩은 안하도록 하는 것이 좋겠죠.^^





반응형


항목 5, 명시적 형식 선언보다 auto 를 선호 하라.


auto라는 형식추론 방식이 C++ 11에서 도입이 되었는데요.

기존의 정적형식 절차적언어들인 C#, D, Scala, Visual Basic)등에서 auto와 비슷한 기능이 있었고, 여러 정적형식 함수형 언어들(ML, Haskel, OCaml, F#)등에서도 지원되는 기능입니다.


Perl, Python, Ruby와 같은 변수 형식을 명시적으로 지정해야 하는 경우가 아주 드문 동적 형식 언어들의 성공으로 인해 c++에서도 전격적으로 도입이 되었다고 보여집니다.


auto로 선언할 경우 힘들어지는 부분은 아마도 type이 바로 안보여서, "추측하기가 힘들다는 것, 가독성(readability)이 떨어진다." 일텐데요.

그렇지만 이런 불편보다 이익을 더 많이 얻을 수 있습니다.


1. 간단한 선언이 다시(?) 가능해졌다.

 template의 사용이 일반화되면서 type에 대한 선언부들이 복잡해지고, 심지어는 compiler에 의해 명시적 타입 지정이 힘들어질 경우도 생깁니다.


template<typename T>

void dwim(T b, T e)

{

  for(; b!=e ; ++b)

  {

    typename std::iterator_traits<T>::value_type curValue = *b;

    :

  }

}


명시적으로 변수 선언을 하려면 type 부분이 너무 길어지게 되는데, 간단한 지역 임시변수의 경우에는 auto 로 사용하는 것이 오히려 가독성과 코드 유지에 도움이 될것 같군요.



2. 타입(type)선언을 컴파일러(compiler)의 도움으로 선언하기 때문에 타입 불일치가 줄어든다.

unsigned int size = v.small_size(); // size는 int type이 됩니다. 64 bit OS에서는 64 bit, 32 bit OS에서는 32bit이 됩니다.


또 small_size()의 return type을 변경했을때, 기존 code로 작성되어있던 부분들에서 오류가 발생할 확율이 높습니다.

그리고 찾아다니면서 변경을 해줘야 겠죠.


반면,

auto size = v.small_size();  //small_size()의 return 값의 타입으로 size가 선언됩니다.

코드 수정 및 오류 확율이 줄어듭니다.


std::unordered_map<std::string, int> m;


for(const std::pair<std::string, int>& p : m)

{

  ...

}


이 경우에, unordered_map 의 key 부분이 const 여야 합니다. 따라서 p를 std::pair<const std::string, int> 가 되어야 합니다.

프로그래머의 실수이기는 하지만, 아무튼 이 상황에서 compiler는 std::pair<const std::string, int> 를 std::pair<std::string, int>로 변환하도록 시도하게됩니다.

이 과정에서 p를 위한 임시객체를 생성하고 m으로 부터 복사를 해옵니다. 

code의 길이에 비해 상당히 복잡한 과정이 발생하게 되는 것이죠.

또 loop이 끝나는 부분에서는 임시객체가 파괴(삭제)되게 되죠.


for(const auto& p:m)

{

:

}


이와 같이 auto를 이용하여 작성을 하게 되면, 이와 같은 임시객체 생성이 발생하지 않고, m 내부의 한 요소를 가리키는 포인터를 얻게 됩니다.

효율적이고 typing도 줄어들게 됩니다.



3. 초기화 되지 않은 변수 사용이 줄어든다.

초기화 되지 않은 변수는 c++ 프로그래밍을 하면서 자주 격는 문제입니다.  이런 문제에 민감한 개발자라도 한두번은 실수 할때가 있는 그런 이슈이죠.

사소하면서도 중요한 언어적인 특성이라고 봐야겠죠.



auto를 사용 하게 되면 이런 부분들이 개선됩니다.

auto 변수는 선언과 동시에 값(타입 과 함께)이 정해져야 하기 때문에 auto 변수 자체가 초기화 되지 않을 가능성은 없습니다.

auto 를 사용할 경우 초기화가 되지 않으면 컴파일(compile) 단계에서 에러를 만나게 되기 때문이죠.

이런 사소한 실수가 줄어들게 됩니다.


다만 auto가 참조(reference)이고 이 참조가 가리키는 변수가 초기화 안되어 있을 경우는 있죠. 

이는 auto 변수의 초기화가 아니라 auto가 가리키는 변수의 초기화 문제로 봐야 하겠죠?





-------------------------------


물론 auto가 만능은 아님은 당연한 것이겠죠..

명시적으로 type을 정의해서 사용하는 것이 좋겠다고 판단한다면 그렇게 하는 것이 좋습니다.


다만 , 기존의 "type을 명확히 하자!!!" 라는 보다는 "auto를 선호하자" 로 C++의 coding style을 옯겨 보는 것은 좋을 것 같군요.



발췌: [Effective modern C++  : 스콧 마이어스 지음, 류광 옮김]

반응형

Tizen 개발 툴중에 CLI라는 것이 있습니다.


Command Line으로 조작할 수 있도록 제공하는 기능인데요.


자세한 내용은 아래 page로 들어가 보시면 확인 할 수 있습니다.

https://developer.tizen.org/development/tools/native-tools/command-line-interface




Tizen IDE에서 현재 프로젝트를 CLI 로 Export 시킬 수 있는 메뉴가 있습니다. (Export to CLI project를 선택하면 됩니다.)



cli를 실행시킬수 있는 프로그램은  <Tizen SDK>/tools/ide/bin 에 위치 합니다.

실행 명령어는 tizen 입니다.


ex) tizen build-native -a arm -c gcc -C Debug 

       tizen tizen-native -a x86 -c gcc -C Debug




build 형식


  tizen build-native [-a {x86|arm}] [-c {gcc|llvm}] 
                     [-C {Debug|Release}] [--]

  • -a, --arch:

    Specifies the architecture type.

  • -c, --compiler:

    Specifies the compiler. You can use this option with the following compiler versions: gcc-4.9 and llvm-3.6

  • -C, --configuration:

    Specifies the build configuration.

  • --:

    Specifies the project directory.



create 형식
  tizen create native-project [-p <profile name>] [-t <predefined template>] 
                              [-n <project name>] [-- <project location>]

  • -p, --profile:

    Specifies the profile name.

  • -t, --template:

    Specifies the template name.

  • -n, --name:

    Specifies the project name.

  • --:

    Specifies the destination directory where the project is created.



  

Tizen SDK의 ide가 아닌 다른 IDE나 editor를  사용한다면 CLI를 이용해서 build 까지 customizing 해서 사용할 수 있습니다.



'tizen' 카테고리의 다른 글

EFL: event flow control (이벤트 흐름 제어)  (0) 2016.08.25
tpk install, 설치  (0) 2014.05.28
Tizen::Content::ContentSearch 사용하기  (1) 2010.05.19
반응형



Object 의 생명주기 (life cycle) 관리에 대해서 고민하다가 아래와 같이 작업을 해보게 되었습니다.


Reference counting 방식의 object 관리에 대한 내용인데, 기존에 object 또는 메모리 allocation 된 내용은 사실 관리하기가 무척 까다롭습니다.

다행히도 요즘에 C++에서  smart pointer 등의 feature를 정식으로 지원해서 좀 편해진 부분들이 있지만, 여전히 관리는 필요합니다. 물론 memory leak 때문 만은 아니고, dangling pointer 의 경우도 해당하죠.

해당 instance가 삭제되었는데 사용되는 경우들을 방지하는 것은 매우 중요하기 때문입니다.

이는 개발자가 머리 속으로 모든 것을 채크해 낼 수 없기 때문에, framework 이나 library 레벨에서 채크해주는 것은 매우 중요합니다.

shared_ptr과  weak_ptr로 대응 할 수도 있지만 약간 색다른 방법으로 접근 해보고자 했습니다.


ex)

class ITest {

  public:

  virtual bool doTest(){return true;} // 순수가상 함수로 만들고 싶었으나 그러면 설명할 코드가 길어질것 같아서 그냥 가상함수로 했습니다.

};


class IWork {

public:

virtual void doWork(){....}

}


class Framework {

public:

:

  void setTest(ITest*test);

  void setWork(IWork*work);

  void run()  {

    if(pTest && pWork ) {

if( pTest->doTest() )

              pWork->doWork();

     }

  }

ITest* pTest;

IWork* pWork;

}




void main()

{

Framework fr2;

ITest* pTest = new ITest;

IWork* pWork = new IWork;

fr2.setTest(pTest);

fr2.setWork(pWork);

delete pWork; <-- pWork가 delete되어도 개발자는 문제를 이 시점에 잡아낼 수 없습니다. fr2에서 사용 중인데도 말이죠.

fr2.run(); <-- 여기서 죽게 되죠.. 

}


이 예제 코드에서 문제를 해결하기 위해서 shared_ptr 과 weak_ptr 로 개선을 해보려 Framework class 내의 변수들을 weak_ptr로 변경 한다고 합시다.


class Framework {

public:

:

  void setTest(std::shared_ptr<ITest> test);

  void setWork(std::shared_ptr<IWork> work);

  void run()  {

    if(pTest && pWork ) {

if( pTest->doTest() )

              pWork->doWork();

     }

  }

std::weak_ptr<ITest> pTest;

std::weak_ptr<IWork> pWork;

}


이렇게 되면 아래와 같은 코드 작성시에 처리하기가 곤란해집니다.


class MyFramework : public Framework , ITest, IWork {

   MyFramework ()  {

    setTest (this); <-- 여기를 어떻게 해야 할지.

    setWork(this);<-- 여기를 어떻게 해야 할지.

  }

}


void main()

{

// case 1

MyFramework fr;

fr.run();

}





그래서 생각해본게 Object 와 ObjectRef 형식의 페어구조입니다.

코드는 아래와 같습니다.


즉  어떤 objectType A가 있다고 한다면.


A를 new 로 생성하고 사용하다가 만약 이 object의 pointer를 어디선가 참조하여 사용하려할때,

A object의 reference 를 증가시키고 이 Object는 Reference count를 채크하여 삭제될때 assert를 내줍니다.

이러면 사용중인 object가 삭제되는 시점을 찾을 수 있게 됩니다.


이 과정을 좀더 자연스럽고 어플리케이션 로직 개발자가 reference count를 의식하여 조작하지 않더라도 동작하도록 하는 부분에 대해서 고민이 필요한데, 이와 관련된 내용을 아래와 같이 정의 했습니다.


ObjectType * pObject = ObjectType;


ObjectRef<ObjectType> ref = *pObect;


이와 같은 형태로 사용하게 되면, 기존에 smart pointer 와 비슷한 형식이 됩니다.

사용상 편의성 역시 큰 차이가 없을것 으로 보여지고 말이죠.



Object와 ObjectRef 의 관계 구현은 아래와 같습니다.


<RefObject.h>

#ifndef __OBJECT_REF_H__

#define __OBJECT_REF_H__


class Object

{

public:

Object();

virtual ~Object();

private:

void addRef(){ __ref++; }

void relRef(){ __ref--; }

int getRef(){ return __ref; }

private:

int __ref = 0;

friend class _Ref;

};


class _Ref

{

public:

virtual ~_Ref();

_Ref();

_Ref(Object& obj);

void set(const Object& obj);

void reset();  // reference를 reset 하는 기능

operator bool();

protected:

Object*__pObject = NULL;

};


template<typename T>

class ObjectRef : public _Ref

{

public:

ObjectRef(){}

ObjectRef(T& o) :_Ref(o){}


T* get(){ return dynamic_cast<T*>(__pObject); }

T* operator ->(){ return dynamic_cast<T*>(__pObject); }

ObjectRef& operator = (const T& obj)

{

set(obj);

return *this;

}


};

#endif //#ifndef __OBJECT_REF_H__

// cpp file

#include <memory>
#include <assert.h>
#include <stdio.h>

#include "objectRef.h"

Object::Object(){}

Object::~Object()
{
assert(__ref <= 0);
}



_Ref::~_Ref()
{
if (__pObject)
{
__pObject->relRef();
__pObject = NULL;
}
}
_Ref::_Ref()
{
}

_Ref::_Ref(Object& obj)
:__pObject(&obj)
{
obj.addRef();
}

void 
_Ref::set(const Object& obj)
{
if (__pObject)
{
__pObject->relRef();
}
__pObject = const_cast<Object*>(&obj);
__pObject->addRef();
}
void 
_Ref::reset()
{
if (__pObject)
{
__pObject->relRef();
__pObject = NULL;
}
}

_Ref::operator bool()
{
return (__pObject != NULL);
}




위 구현 로직을 바탕으로 테스트용 셈플을 작성해봤습니다.


<test.cpp>

#include <stdio.h>

#include "RefObject.h"


namespace

{


class Do : virtual public Object

{

public:

virtual void onDo(){ printf("onDo()\n"); }

};


class Done : virtual public Object

{

public:

virtual void onDone(){ printf("onDone()\n"); }

};



} //namespace


void 

main()

{

Do* pDo = new Do;

Done* pDone = new Done;


pDo->onDo();

pDone->onDone();


ObjectRef<Do> doRef(*pDo);

ObjectRef<Done> doneRef(*pDone);


doRef->onDo();

doneRef->onDone();


doRef.reset();

delete pDo;

delete pDone; //<-- error occurred


}



main 에서 doRef.reset() 을 Reference 를 reset한 경우에는 delete가 정상적으로 되지만, 그렇지 않은경우 delete 시에 assert가 발생합니다. 

즉, 사용하고 있는 곳이 있는데 어디선가 delete를 시도 한다면 reset을 발생시켜주는 코드입니다.



<test2.cpp>


#include <memory>

#include <assert.h>

#include <stdio.h>

#include "objectRef.h"


namespace {


class IDo : virtual public Object

{

public:

virtual void onDo() = 0;

};


class IDone : virtual public Object

{

public:

virtual void onDone() = 0;

};



class MyDo : virtual public Object, virtual public IDo, virtual public IDone

{

public:

virtual void onDo()

{

printf("hello !\n");

}

virtual void onDone()

{

printf("bye !\n");

}

};




class Job

{

public:

void setJob(IDo* job)

{

instDo = *job;

}

void setJobNoti(IDone* jobnoti)

{

instDone = *jobnoti;

}


void doWork()

{

if (instDo)

{

instDo->onDo();


if (instDone)

instDone->onDone();

}

}

void reset()

{

instDo.reset();

instDone.reset();

}


ObjectRef<IDo> instDo;

ObjectRef<IDone> instDone;


};


}


void

main(void)

{

std::unique_ptr<MyDo> pMyDo(new MyDo);


Job j;

j.setJob(pMyDo.get());

j.setJobNoti(pMyDo.get());


j.doWork();


// j.reset();

delete pMyDo.release();


j.doWork(); // <-- error occurred

}







'개발 Note > Codes' 카테고리의 다른 글

[Andriod] Timer and TimerTask  (0) 2020.10.22
Singleton class 설계  (0) 2020.10.07
sorting algorithms  (0) 2014.02.26
c++ while 문 - 잘 안쓰는 표현  (0) 2013.10.23
UML2 Sementics  (0) 2012.01.11
반응형

오류 검증 문제

 

M3는 유용하지만 실행되서는 안되는 프로그램들이 있습니다. 실행중에 타입이 맞이 않아서 실행을 멈추게 되는 경우를 가진 프로그램들입니다.

 

타입

 - 프로그램을 기획하는 한 방법

 - 프로그래밍 언어가 그러한 기획을 물샐틈 없이 할 수 있도록 구성되어야 

  "너무 빡빡하지 않게" (PASCAL, PL/1, Algol68, Ada)

 

프로그램이 기획한 대로 실행된다는 것을 보장해야

 

프로그램 기획이 제대로 됬는지를 실행전에 검증 될 수 있어야 

검증이 자동으로 된다면...

 

 

M3 프로그램은 다섯종류의 값들이 있고 각각 분별력있게 흘러다녀야 합니다. 함수, 정수, 참/거짓, 쌍, 메모리 주소 입니다.

1. 함수 적용식  E1 E2  에서 식 E1은 함수여야 합니다. 

2. 덧셈식 E1 + E2 의 부품식들의 결과는 정수여야 합니다.

3. 조건식 if E1 E2 E3 에서 E1의 결과값은 참/거짓 이어야 합니다.

4. 쌍에서 첫번째 값을 뜻하는 식 E.1 에서 E의 결가값은 쌍이어야 합니다.

5. 메모리에 쓰는 식 E1:=E2 에서 E1의 결과 값은 메모리 주소여야 합니다.

 

M3 프로그램이 위와 같은 타입의 조건을 실행중에 항상 만족하는지를 미리 자동으로 검증하는 것이 가능했으면 하는 것입니다.

 

미리 static 안전하게 sound 검증하는 그러한 타입 시스템이 M3에 대해서는 가능합니다.

 

정적 타입 시스템 static type system

 

정적 타입 시스템은 말이 되는 프로그램인지를 프로그램 텍스트만으로 판단하는 한 방법입니다. 실행전에 말이죠.

이는 정적 의미 구조 static semantics 라고 부르기도 합니다. 이전까지의 의미구조들은 모두 동적 의미구조 dynamic semantics 였습니다.

 

일차적으로 문법 검증이 수행되는데, 

대부분 문법 구문은 아주 간단하기 때문에 문법 자체를 검증 하는 것은 쉽습니다.

그러나 프로그램은 문법 검증만으로 안전하다는 보장은 할 수 없습니다.

 

예를 들면,아래와 같은 간략한 문법규칙이 있다고 합시다.

                          

 

문법 규칙이 간단하다는 것은 문맥을 생각하지 않는 규칙들이기 때문입니다.

+ 식은 두개의 부품식들이 정수식이어야 한다는 이런 문맥에 대한 조건은 "문법 규칙"에 표현하지 않습니다.

그래서  1+'a'는 문법상으로 정상이 되는 것입니다.

만약 이런 문맥에 대한 조건들을 표현한다면, 문법 규칙에서 "정적 타입 시스템"으로 은근 슬적 넘어가는 것입니다.

 

정적 타입 시스템 은 결국 일종의 정적 프로그램 분석(static program analysis)입니다.

대부분의 프로그램 분석이 그렇듯 정적 타입 시스템 역시 완전하지 못합니다.(incomplete)

그러나 안전하기는 합니다.(sound) 안전하도록 타입 시스템을 고안 해야 합니다.(우리 언어인 M3안에...)

 

정적타입 시스템은 형식 논리 시스템(formal logic)입니다. 논리식의 생김새, 논리식의 의미, 참인 논리식을 기계적으로 추론하는 규칙들 proof rules 또는 inference rules라고 불리는 것들 을 이용하여, 안전성과 완전성을 증명하는 논리 식들로 구성하는 것입니다.

 
그렇게 디자인이 끝나면, 구현합니다. 
구현된 타입시스템은 대상 프로그래밍 언어로 작성된 임의의 프로그램을 입력으로 받아 타입 오류가 있을지 없을지를 검증합니다.
 

구현되는 알고리즘이 디자인 한 타입 시스템을 제대로구현한 것이라는 사실도 확인하게 됩니다. 디자인에서 구현까지 단단한 과정을 밟는 것입니다.

 

 

형식 논리 시스템(formal logic) 리뷰

 

형식 논리 시스템은 논리식 집합의 정의, 논리식 의미의 정의,  참논리식 집합의 정의, 참논리식 추론의 방법, 추론방법 평가하기

로 구성됩니다.

 

 

선언 논리 (propositional logic) 시스템을 보자. 논리식 집합은 다음과 같은 귀납 규칙으로 정의됩니다.

 

                                    

 

논리식의 정의는 다음과 같고,

 

                    

 

 

 

참인 논리식들의 집합을 정의합니다 

: 즉, 쌍 ({f1,...,fn},f)    (표기 : 

)들의 집합입니다.

 

참인식 

들의 집합들.

 

 

        

 

 

 

                          

 

 

        

 

 

                       

 

 

                                

 

 

 

이 규칙들은 참인 식을 만드는 규칙이고, 이것을 논리 시스템에서는 추론규칙 inference rules 혹은 증명규칙 proof rules 라고 합니다.

 

여기서 살짝 다른 관점에서 보자면, 참인 논리식 집합을 만드는 과정은 곧 참 논리식을 유추한 증명을 만드는 과정이기도 합니다. 증명들의 집합을 만드는 귀납규칙으로보는 것입니다. 

 

증명규칙으로 만들어지는 증명을 증명 나무 (proof tree)라고 합니다.

 

이제 이렇게 "기계적인" 증명규칙 혹은 추론 규칙이 정말 좋은가를 따져봐야 합니다.

 

추론 규칙의 안전성 soundness

 

 

추론 규칙의 완전성 completeness

 

 

 

 

단순 타입 시스템 simple type system

 

 

M0 로 모든 것을 프로그래밍 할수 있겠으나, 값은 오직 함수 밖에 없었습니다. 값의 타입으로 함수와 정수만 있는 M1 코어만 생각합시다.

                                

위의 의미 규칙

 

                                

 

를 사용할 수도 있으나, 타입 시스템의 안정성 증명에서 편리한 방식을 위해서 프로그램 텍스트를 다시 써가는 방식의 의미에서, 

의미는 같지만, 실행 문맥 evaluation context을 이용하여 다음과 같이 정의 합니다.

 

 

 

실행 문맥은 적극적 실행 Eager evaluation 순서에 준해서 다음에 실행해야 할 부분을 결정됩니다.

프로그램 실행 규칙은 다음과 같습니다.

 

 

                             

 

                          

 

                                  

 

프로그램 E의 의미는 위의 규칙에 따라

            

                                     

 

 

단순 타입 추론 규칙

 

타입시스템을 정의합시다.

다시 한번 강조 하지만, 프로그램 텍스트만을 가지고 타입 오류 없이 실행되는 프로그램인지를 검증하는 논리 시스템입니다.

-프로그램 텍스트에 타입이 명시된것은 없습니다.

 하지만 논리시스템은 프로그램 구석구석의 타입이 어떻게 기계적으로 유추될 수 있는지를 정의합니다.

 

 

                  

 

논리식의 생김새는 

                             

입니다.

 

Γ(gamma)는 타입 환경 type environment 으로 변수들의 알려진 타입을 가지고 있습니다.

 

                    

 

타입환경 Γ에 대해서 Γ{xτ} 대신 Γ+x:τ로도 씁니다.

xτ ∈ Γ 대신에 x:τ ∈ Γ 로도 쓸 것입니다.

 

논리식의 의미는

                  [[ Γ⊢E:τ]]= true

                              iff

    

                 : σ  Γ.E 이 영원히 돌든가, 값을 계산 E→*υ 하면 υ:τ

입니다.

 

이제 참인 논리식을 유추하는 규칙을 정의합니다.

타입 추론 규칙 type inference rules

 

 

                                          

 

                                         

 

 

                                

 

 

                     

 

이 식을 이용해서 실제 타입들에 대해서 증명과정에 대해서는 생략...

 

 

1. 식 E의 생김새마다 오직 하나의 규칙이 있다.

 이 사실은 증명규칙의 성질을 증명할 때 우리를 편하게 합니다.

예를 들어

이런 식이 유추 되었다면, 반드시 한 경우밖에 없습니다. : 

의 타입 유추 규칙이 하나 밖에 없으므로, 그 규칙에 있는 조건이 만족한 경우 밖에 없습니다.

즉, 

 

이면   

          

 이면 

                                             :

 

 

2. 어떤 식 E에 대해서, Γ⊢E:τ 인 τ값이 여럿 가능하다.

 

3. 문제 없이 실행되는 프로그램이 타입 유추가 불가능한 경우가 있다. 완전 complete 하지는 못한 것이다.

 

 

 

 

추론 규칙의 안전성

우리는 추론 규칙의 안전성 soundness은 증명할 수 있습니다.

즉, 타입 추론이 성공하면 그 프로그램은 타입 오류 없이 실행된다는 것이 보장됩니다.

즉, 프로그램(자유변수가 없는 식) E에 대해서

                                   

이 추론될 수 있다면, 프로그램 E는 문제 없이 실행되고 , 끝난다면 결과값 τ 타입이라는 것입니다.

 

두가지 증명법

1. 안정성을 증명하는 한가지 방법.

- Progress Lemma: 값이 나올 때 까지 문제 없이 진행한다.

               ⊢e:τ 이고 e가 값이 아니면 반드시 e  e'

- Subject Reduction Lemma : 진행은 타입을 보존한다.

               ⊢e:τ 이고  e  e' 이면  ⊢e':τ

 

 

 

2. 안정성 증명하는 두번째 방법.

- E → error 를 정의합니다.

- Subject Reduction Lemma : "진행은 타입을 유지한다", 를 증명합니다.

      ⊢E:τ 이고 E E' 이면 ⊢E':r 이다.

- 안정성이란, 값이 아닌 식 E가 타입이 있으면, E는 문제없이 진행하며 끝난다면 그 타입은 값이어야 한다.

- 값이 아닌 식 E가 타입이었다고 하자. 잘 진행하는가?

   그렇다, E

→error로 진행할 수 없다. 왜냐하면, 그렇게 진행한다면 "Subject Reduction Lemma"에 의해서 모순이기 때문이다. error가 타입이 있어야 하는데 error의 타입을 결정하는 규칙은 없기 때문이다.- 그리고 진행이 타입을 항상 보존하므로, 값으로 진행이 끝나게 되면 그 값도 같은 타입을 가진다.

 

 

 

이 단순 타입 시스템은 논리시스템으로 우리가 바라는 바를 가지고 있음을 증명할 수 있었습니다. 

다음 단계는 구현입니다. 하지만 간단해 보이지 않습니다. 다음 규칙을 보면 말이죠.

                                        

 

 

함수 몸통 E를 타입 유추하려면 인자의 타입 τ1을 알고 있어야 합니다. 그러나, τ1은 우리가 최종적으로 유추해야 할 함수 타입의 일부입니다.

어디서 본듯한 패턴입니다. 유추해야 할것을 미리 알고 있어야 한다.!!! 유추를 포기한다? 프로그래머에게 함수마다 타입을 기입하라고 해야 할까?

 

이번에는 놀라운 방식이 있습니다. 타입에 대한 연립방정식을 세우고 풀어가는 과정입니다.

그 과정이 놀라운 이유는 ,우선 타입을 자동으로 유추해 주는 알고리즘 때문입니다. 프로그램 텍스트에 타입에 대해서 프로그래머가 아무것도 명시할 필요가 없습니다. 자동으로 유추되기 때문입니다.

또다른 이유는, 타입 시스템을 충실히 구현한 알고리즘이기 때문입니다. 충실히?? 타입 시스템이 유추할 수 있는 것을 그 알고리즘은 똑 같이 유추해줍니다. 그 반대도 성립합니다. 알고리즘이 유추해 내었으면 타입 시스템도 같은 것을 유추해 낼 수 있습니다. 서로 iff관계로 논리시스템과 구현 시스템이 물려 있습니다.

 

예를 들면,

   1+(λx.x 1)0

이런 식이 있다고 합시다.

 

 

 각 부품(파트) 별로 번호를 붙여봅시다.

 

 

부품식 i 가 가져야 하는 타입 αi 와 변수 x가 가져야 하는 타입 αx에 대한 방정식 "lhs ≐ rhs" 는 다음과 같습니다.

 

 

 

위의 방정식의 해는 없다.  αx 는 ι(iota 요타)이기도 해야 하고 ( α αx 로부터) ι →ι이기도 해야 하므로 ( α6 αx 로부터)

 

 

 

타입 연립 방적식 u는 다음과 같은 모습입니다.

 

타입 방정식

연립

타입변수

 

 

타입 연립 방정식의 해 S를 치환으로 표현하면 편합니다. TyVar을 Type으로 바꾸는 것입니다.

 

                                      

:A->fin B  = A에서 B로 가는 치환들의 집합입니다. 

따라서 TyVar에서 Type으로 가는 집합을 의미합니다.

 

온라인 알고리즘들

타입 방정식을 도출하면서 그때 그때 풀어가는 알고리즘도 가능합니다.

 

 

 

 

안전한 그러나 경직된

 

단순 타입 시스템은 안전하긴 하지만 아쉬움이 많습니다.

완전하지 못하다. 타입 오류 없이 잘 실행될 수 있는 모든 프로그램이 단순 타입시스템을 통과 할 수는 없습니다.

인자 타입에 상관없이 실행되는 함수들이 많이 있습니다.

안전하지만 빠뜨리는 프로그램들이 있는 것입니다.

 

 

재귀 함수

재귀 함수는  Y 컴비네이터  (Y combinator)를 통해서 표현할 수 있습니다.

 

                            

  :Y 컴비네이터

이 핵심 부분은 자신을 인자로 받는 함수의 적용  "x x"입니다.

단순 타입 시스템에서는 함수가 자신을 인자로 받는 식은 타입 유추가 될 수 없습니다.

 

                             

 

각 부품식 i가 가져야 하는 타입 αi를 따져보면,

 

 

이 되는데, 결국 α→βα를 만족하는 타입을 Type에서는 찾을 수 없습니다.

unification  알고리즘은 위의 양변을 같게 만드는 α와 β를 찾는 것에 실패한다.

 

단순 타입시스템이 갖추어진 언어에서는 재귀함수를 Y 컴비네이터로 표현해서는 타입 시스템을 통과할 수 없습니다.

 

때문에 재귀함수인

                                      

은 필수가 됩니다. (더이상 설탕이 아닙니다.)

 

 

 

메모리 주소 값

메모리 주소를 값으로 사용하는 경우는 타입 시스템을 어떻게 확장할 수 있을까?

 

                                   

 

 

우선 타입의 종류가 하나 늘어납니다.

 

 

 

1. 타입 τ loc 는 메모리 주소타입인데, 그 주소에는 τ 타입의 값이 저장되는 타입입니다.

그리고, 타입 규칙들은 자연스럽게 확장됩니다.

 

 

 

 

 

 

 

 

 

 

다형 타입 시스템

 

단순 타입시스템을 정교하게 확장하자.. 안정성을 유지하면서 "잘 모르겠다"고 하는 경우를 줄입니다.

안전하면서 유연한 타입시스템이 필요합니다.

다형 타입 시스템(polymorphic  type system)이 바로 그러한 타입시스템입니다.

타입 유추가 가능하고 실제 언어에 실용적으로 구현될 수 있는 다형 타입 시스템이 let-다형 타입 시스템입니다.

 

타입 시스템에서 

"잘 모르겠다" = "타입방정식의 해가 없다" 즉,

 

이런경우 ⊢p 는 ⊢를 포섭하면서 확장한 경우라고 합니다.

 

다형 타입 시스템에서 "잘 모르겠다"고 하는 경우가 단순 타입 시스템 보다는 적습니다.

 

 

 

 

 

 

 

 

반응형



프로그래밍 언어의 편의성 측면에서는 여러가지 설탕 구조물들이 첨가 되어야 합니다. 

이는 프로그래머에게 편의를 제공해주고, 코드의 이해를 돕는데 좋은 장치가 됩니다.


컴퓨터 메모리를 사용하는 명령형 언어의 모습(imperative features)가 그 대표적인 예입니다.

추가합니다.  

언어키우기 : M3




1. 새로운 메모리 주소를 할당받는다.

2. 메모리 주소에 저장된 값을 읽고 쓴다.

3. 프로그램 실행 순서에 따라서 다른 결과를 계산하게 될 수 있다. (주소에서 읽고 나서 쓰느냐 쓰고나서 읽느냐)


이제 값의 공간에는 메모리 주소가 포함되었습니다.




메모리 주소가 값이 되면서, 프로그램 식의 의미 판단에는 메모리가 필요합니다.

메모리에는 프로그램의 식들이 계산되면서 일어난 반응들이 계속 쌓여갑니다.



  : 식 E가 환경 σ(sigma) 와 메모리 M에서 υ를 계산하고 그 결과는 M'이다.


메모리는 주소에서 값으로 가는 유한 함수입니다.



의미 규칙은 다음과 같습니다.



 



                                  



           



                            


다른 모든 식들의 의미 규칙에도 메모리 반응이 쌓여가는 것이 표현되야 할 것입니다. 예로






이렇게 해서 M3의 문법을 다시 정리하면.

  

                  



while E do E 역시 설탕구조입니다.

우선 M3로 녹일 수 있습니다.(표현 가능합니다.)


다음 >> 정적 타입 시스템 (static type system)



반응형

지금까지 프로그래밍 언어가 어디서 시작되어 어떻게 만들어 졌는지에 대해서 언급했습니다.


현재 프로그래밍 언어가 나아가는 방향은 시스템(기계) 을 다루는 단계에서 점점 본연의 목적을 향해 가고 있습니다.

그 본연의 방향이라는 것은 적어도 "기계를 편하게 다루는 것"은 아닙니다. 

"기계의 편리한 사용" 이라는 슬로건으로는 달성할 수 없었던 결과를 향하는 것입니다.


다시한번 처음에 언급했던, 프로그래밍 언어가 컴퓨터를 구동시키기 위해 만들어 졌는가?에 대해서 되세겨봅시다.

프로그래밍 언어는 컴퓨터를 동작시키기 위해서 만들어진 것이 아닙니다. 프로그래밍 언어가 있었고(수학적 증명을 위해서 만들어진), 이것을 동작시키기 위해서 컴퓨터가 탄생했습니다. 


1930-40 년대에 이미 논리학자와 수학자들은 기계적으로 계산가능한 것이 무엇인지 고민하기 시작했습니다.

괴델은 부분 재귀 함수(Partial Recursive Function)꼴로 정의 되는 함수들을 기계적으로 계산 가능한 것들이라고 정의했습니다.

처치는 람다 계산법(Lambda Calculus)으로 계산될 수 있는 것들이가고 정의 했고,

튜링은 튜링 기계(Turing Machine)가 실행할 수있는 것들이라고 정의 했습니다.


그런데, 세 가지가 모두 같은 정의였습니다. 부분 재귀 함수는 람다 계산법으로 계산될 수 있고, 람다 함수는 튜링 기계로 실행할 수 있고, 튜링 기계가 실행하는 함수는 부분 재귀 함수 꼴로 정의 할 수 있습니다.


그러고 나니 사람들은 기계적으로 계산 가능한 함수가 그게 다가 아닐까 믿고 있습니다. 세사람이 독자적으로 정의한 것들이 결국 다르지 않은 것으로 미루어 , 이것을 "Turing-Church Thesis"라고 부릅니다.


이 셋중에 람다 계산법( Lambda Calculus)이 문법과 의미정의를 가춘 언어의 모습을 하고 있습니다.


람다 계산법 Lambda Calculus


이 람다 계산법이라는 언어를 기초로 프로그래밍 언어를 디자인해가면 , 이 언어의 표현력이 완전하기 때문에 , 기계적으로 계산 가능한 모든 것이 이 언어로 작성할 수 있기에, 든든해집니다.

기계적으로 계산 가능한 모든 것을 표현할 수 있는 언어 "Turing-Complete"이라 합니다.


언어의 이름을 람다(Lambda)라고 합시다.

람다의 문법구조 Syntax 다음과 같습니다.(매우 간단하죠)



                                       



1. x는 이름입니다.

2. 는 함수를 뜻합니다. x는 함수의 인자 이고, E는 함수의 몸통입니다. x의 유효범위는 E입니다. E에 나타난 "x를 묶어준다고(binding)" 표현합니다.

3.E E를 다시 적어보면, E1 E2 로 표현된  함수를 적용하는 식입니다.  

      E1은 계산하면 함수 가 되어야 하고 E2는 그함수의 인자 x의 실체가 됩니다.

     (이 과정을 Beta-reduction이라고 합니다.)

풀이 과정은 주로 Beta-reduction으로 정리 되는데, 즉 람다 함수의 인자인 x에 대입하는 과정이라고 이해하면 되겠습니다.





문맥구조( context) C 는 빈칸[]을 딱 하나 품고있는 람다식입니다.


                                     






아래의 간단한 수식(?) 들을 이용하여 표현해 개념을 이해하고 넘어가겠습니다.



  

(1을 더하는 함수)



(2를  곱하는 함수 )



덧셈 (A) 곱셈 (M)  제곱(P)

(Am)n = m+n

(Mm)n = m*n

(Pm)n=n^m

실제 처치가 람다 계산법에서 연산식을 정의 해 놓은 내용입니다.



처치의 2와 3 같은 숫자는 두번 ,세번 과 같은 의미를 갖습니다.

그래서 

2 =  λfx.f(fx)

3 =  λfx.f(f(fx))

1 =  λfx.fx

0 =  λfx.x

와 같습니다. 

즉 f를 몇번 반복했는가가 의미가 있는 것입니다. 마치 숫자를 연산자나 함수처럼 다루는 것이죠.


예제로 3에 2승 을 계산 해봅시다. 


(P2)3 = ((λfg.fg)2)3

           = (λg.2g)3                         ----------  2g = (λfx.f(fx))g 2g는 g를 2번 수행하는 것 

           = (λg.(λfx.f(fx))g)3   = λfx.f(fx)3

           = λx.3(3x)  ------ (3x) 를 y로 치환하면, 3(3x) = 3y , 즉 y를 3번 수행하는 식이 필요함. (λfy.f(f(fy)))(3x)

           = λx.(λfy.f(f(fy))(3x))

           = λx.(λy.(3x)( (3x)( (3x)y) ) )

           = λxy. (3x)( (3x)( (3x)y) )

           = λxy. (3x)( (3x)( (x(x(xy)) ) )

           = λxy. (3x)( (x(x(x (x(x(xy))))) ) )

           = λxy. (x(x(x(x(x(x (x(x(xy))))))))) = 9 = 3^2



(3x)y  =  (&fz.f( f( fz ) ) x )y= (&z.x(x(xz)))y = x(x(xy)))



이런 Beta-reduction 과정에서   (λx.E)E1 과 같이 연산( 대입) 이 가능 한 부분을 레덱스 (redex)라고합니다.( reducible expression)

이 Beta-reduction 은 어떤 식에 따라서 영원히 계속될 수도 있습니다.

더이상 레덱스가 없을때 연산은 끝납니다. 이런 람다식을 정상식(normal term)이라고 부릅니다.



이 Beta-reduction 과정도 어떤 순서로 하는가에 따라, (즉, 어떤 레덱스 부터 바꾸는가에 따라) 결과가 달라집니다.

그래서 순서가 중요합니다.

정상순서로 계산하는 것은 normal-order reduction 이라고 하고, 제일 왼쪽 제일 위의 레덱스를 계산해가는 것입니다.

이 순서로 진행하면, normal term이 있는 람다식은 항상 그 정상식에 도달합니다.



여기서 의문점이 있을것인데요.

람다로 과연 프로그램 다운 프로그램을 짤 수 있을까요?

이 의문은 지금까지 다룬 식들이 대부분 산술 연산이었기 때문에 나오는 질문일 것입니다.

우리가 흔히 프로그래밍 이라고 하는것은,

1. 어떤 조건에 따라 분기를 해야 하고, 조건에 따라 다른 기능이 수행 되는 것을 의미할 것입니다.

C 코드로 보면,

if (a==10)

    {c=20;} 

else 

    {c=0;} 

흔히 이런 코드를 

    1+1 

보다 프로그램 답다고 생각 할 것입니다.

(당연하죠. 조건문이 논리식이고 그 논리 식에 따라 코드가 분기 되는 것이지만, 그것은 매우 저 수준의 생각이고, 흔히 조건 자체를 논리로 보기 보다는 어떤 상황이나 상태로 보는 경향이 있기 때문일 것입니다. 뭐 여하튼, 우리가 언어의 base를 다루기 때문에 이런 것도 짚어봐야겠죠.)


다시 예기 하면, 논리 식에 따라 코드 분기가 가능한가? 라는 질문으로 단순화 시켜볼 수 있을것입니다.

그 식을 if e1 e2 e3  라고 하고, e1이 true이면 e2를 아니면 e3를 처리하면 되겠군요.


그전에 람다 언어에서 true 와 false에 대해서 정의가 필요합니다.


true = λx.λy.x

false = λx.λy.y

입니다.


하는김에 몇개 더 가져와 보겠습니다.

not = λb.λx.λy.byz

and = λb.λb'.λx.λy.b(cxy)y

iszero = λn.λx.λy.n(λz.y)x  or  λn.n (λx.FALSE) TRUE

succ = λn.λf.λx.f(nfx)




자 이제 준비가 되었습니다.


if e1 e2 e3  -> (e1 e2) e3

                  -> e1' e2 e3

                          1)  -> true e2 e3

                          2)  -> false e2 e3


1) true e2 e3  = (λx.λy.x)e2 e3

                  = (λy.e2) e3  ----> beta reduction 수행을 위해서 e3를 y에 집어넣으려 하지만 몸체에는 y가 없기 때문에 사라짐.

                  = e2


2) false e2 e3 = ( λx.λy.y) e2 e3  ------------> e2를 x에 대입. 그러나 x가 없음 e2는 사라짐

                  = (λy.y)e3

                  = e3



if e1 e2 e3 --> iszero e1 e2 e3


이렇게 해보니 그럴듯 하죠 . 언어같죠.. 람다 문법은 굉장히 단순하면서 프로그래밍 언어가 가지는 요소들을 다 품고 있습니다.


loop 을 구현하기 위해서는 기본적으로 재귀호출이 되어야 합니다.

아래와 같은 형식으로 람다에서 구현이 가능합니다.


In ML, C, Java & etc.

fun fac(n) = 

          if n=0 then 1

          else n*fac(n-1)


In λ-Calculus

      fac = Y(λf.λn. if n=0 1 n*f(n-1) )

      Y = λf.(λx.f(x x))(λx.f(x x))


Then 

     fac  n -> n!



언어 키우기.. M0

람다를 프로그래밍 언어로 바라봅시다. (이글 초반에 이미 그러자고 예기 했었죠? ^^)

λx.E 는 함수 정의로 봅시다. 그런데 함수 이름은 없습니다. 인자가 x이고 몸통이 E인 함수입니다. E1 E2는 함수를 적용하는 식입니다.

람다에서 계산과 프로그램에서의 실행은 조금 다릅니다. 람다에서 계산의 끝은 식의 모든 구석구석에 레덱스가 없는 경우입니다. 

함수식 λx.E 의 몸통 식 E에도 레덱스가 있다면 몸통식은 계산이 됩니다.



프로그램 에서는 λx.E 가 최종 값입니다. 몸통 E의 실행은 그 함수가 호출될때 비로소 시작됩니다.

이 최종값인  λx.E를 기준식 (canonical term)이라고 부릅니다.

기준식이 값이기 때문에 종종 υ("value" : upsilon)로 표기 합니다. 



소극적 실행 Lazy evaluation 과 적극적 실행 Eager evaluation


앞에서 β- reduction 과정에서 순서가 중요하다는 예기를 했었는데, 그것과 관련 있는 예기입니다.

프로그램이 실행되면서 함수는 자체로 값이 됩니다.  함수의 몸통은 그 함수가 호출될때 비로소 실행될 뿐입니다.


여기서 함수가 호출될때 E1 E2 ,  인자식 E2를 언제 실행해주기로 해야 할까요?

두가지 선택이 있을 것입니다. 몸통을 실행하면서 인자 값이 필요할 때에 인자 식을 실행하거나, 몸통을 실행하기 전에 인자 식을 실행해서 인자 값을 구한 후에 몸통을 실행하거나. 이 두가지 선택을 할 수 있을 것입니다.


첫번째 경우를 소극적 실행 Lazy evaluation, normal-order evaluation , 또는 식 전달 호출 방식 call-by-name, call-by-need 라고 합니다.

두번째 방식을 적극적 실행 Eager evaluation 혹은 값 전달 방식 call-by-value 라고 합니다.


람다 언어(우리가 람다 계산식을 바탕으로 키워가고 있는 언어) 에서 실행 방식을 정의하는 규칙은 다음과 같습니다.


                     



                          



                                       Lazy evaluation

                               Eager evaluation



각각의 장단점이 있습니다.

소극적인 실행으로 적극적인 실행 보다 빨리 계산 되는 경우가 있고, 반대의 경우도 있습니다.


소극적으로 실행하면

   (λx.7)((λx.x x)(λx.x x)) =>N 7

이지만 적극적으로 실행하면

(λx.7)((λx.x x)(λx.x x)) =>E (λx.7)((λx.x x)(λx.x x))

                                   =>E :

영원히 돌게 됩니다.(무한 루프)


반면,

아래를 소극적으로 실행하면,

   ((λx.(x..x))E =>N (E..E) =>N .....

E를 두번 실행해야 하지만,적극적으로 실행하면, 한번만 실행됩니다.

((λx.(x..x))E =>E (λx.(x..x)) υ =>E ( υ.. υ) =>E ...



람다언어의 문법을 시작합시다.



                



1. 이 언어에서 이름 지을 수 있는 것은 값 뿐입니다. 이것을 변수라고 합니다.

2. 변수 x 의 유효범위는 그 이름을 묶은 함수 λx.E 의 몸통 E입니다.

3. 각 변수가 무슨값을 뜻하는지는 그 변수를 묶은 함수가 호출될 때 전달되는 인자 값이 그 변수가 뜻하는 값이 됩니다.


의미 정의는 프로그램 텍스트를 변화시키지 않으면서 정의합시다.


                    

"환경 σ(sigma) 에서 식 E는 값 υ를 계산한다" 는 뜻힙니다.


의미정의에서 환경을 따로 가지는 이유는 프로그램 식을 변경하지 않기 때문입니다.

변수는 그대로 프로그램에 남아 있는 것이죠. 예전처럼 프로그램 이름이 텍스트에서 해당 값으로 바꿔써지는 방식이 아닙니다.

값은 정수와 함수 뿐입니다. 

함수 값을 클로져(closure)라고 하는데, 함수  λx.E 텍스트 자체와 그 함수가 정의될 때 (static scope)의 환경입니다.


환경의 역할은  λx.E에서 자유로운 변수들의 값을 결정해주는 것입니다.



           



의미 규칙들은  적극적인 실행 규칙(Eager evaluation)을 같습니다.



언어키우기 M1

M0 를 가지고 모든 프로그램을 짤 수 있지만 불편합니다.

프로그래밍의 편의를 위해서 설탕을 좀 첨가할 필요가 있습니다. 설탕구조(syntactic sugar)

 

정수, 참/거짓


추가하고 싶은것들은 정수, 참/거짓, 재귀함수 rec f λx.E, 조건식 if E E E, 그리고 덧셈식 E+E

동치식  E=E. 등입니다.



                               




가령 let x=E1 in E2  의 경우  (λx.E2)E1 이지만 사용하기 편리하게 그 자체로 그대로 둡시다.


이제 값들은 세종류가 되었습니다. 함수값과 정수 그리고 참/거짓



                               



 구조가 있는 값 : 쌍 pair

구조를 가진 데이타를 프로그래밍하기 쉽게 하자.

쌍을 만들고 사용하는 방식을 제공합니다.


                                           


이제 값들은 세가지 종류가 있습니다. 함수값, 정수, 참/거짓,혹은 두값의 쌍



쌍을 M0로 표현하면

(E1,E2) =  λm.(mE1)E2

E.1 = E( λx. λy.x)

E.2 = E( λx. λy.y)

로 풀어서 쓸수 있습니다.


이 쌍을 이용해서 리스트, 나무구조(tree), 그래프도 표현할 수 있고 함수나 테이블도 표현할 수 있습니다.

리스트를 구현해보면 다음과 같습니다.

     λx.λlst.(x,lst)

"link 1 nil" 은 1 하나있는 리스트[1]

"link 1 (link 2 nil)" 은 [1,2]인 리스트를 만듭니다.


isNil?                              head                   tail           

λlst.(lst=nil)                    λlst.(lst.1)          λlst.(lst.2)




두갈래 나무구조 binary tree 를 구성해봅시다.

empty                     leaf              node

0                              λx.x                λlt. λrt.(link lt rt)


isEmpty?                 left                right

 λt.(t=empty)         λt.(t.1)          λt.(t.2)




다음 >> 값 중심의 언어- 메모리 주소 값 : 명령형 언어의 모습




+ Recent posts